[isabelle-dev] Function package produces "duplicate rewrite rule" warnings

[Brian Huffman]

The datatype package produces some extra warning messages now too:

### Ignoring duplicate rewrite rule:
### True == induct_true

### Ignoring duplicate rewrite rule:
### False == induct_false

I haven't checked, but I would be willing to bet that this behavior
was introduced by the same changeset as the function package warning
messages. I wouldn't be surprised if warnings pop up in other packages
as well.

- Brian


On Mon, May 3, 2010 at 12:48 PM, Alexander Krauss <krauss at in.tum.de> wrote:
> Hi Brian,
>
> Thanks for bisecting this, I'll have a look.
>
> Alex
>
> Brian Huffman wrote:
>>
>> Recent versions of the function package produce some unhelpful warning
>> messages about duplicate rewrite rules:
>>
>> ### Ignoring duplicate rewrite rule:
>> ### Sum_Type.Projl (Inl ?y) == ?y
>>
>> ### Ignoring duplicate rewrite rule:
>> ### Sum_Type.Projr (Inr ?y) == ?y