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

[Brian Huffman]

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

I discovered the warnings when using Library/Nat_Bijection.thy, but as
far as I can tell, every invocation of the "fun" command now produces
a similar warning.

I did a search using "hg bisect" and identified the following revision
as the source of the problem:

The first bad revision is:
changeset:   36594:5c5b5c7f1157
parent:      36560:8da6846b87d9
user:        wenzelm
date:        Fri Apr 30 17:18:29 2010 +0200
summary:     conditional warnings: explicitly observe context
visibility flag, not just accidental presence of a context;

http://isabelle.in.tum.de/repos/isabelle/rev/5c5b5c7f1157

The specific rules mentioned in the warning message are used in
HOL/Tools/Function/sum_tree.ML:

val proj_in_rules = [@{thm Projl_Inl}, @{thm Projr_Inr}]

In turn, "proj_in_rules" is used in HOL/Tools/Function/mutual.ML as
part of function "recover_mutual_psimp", where those rules are
explicitly added to a simpset. Since the rules are (usually) already
in the simpset, it produces a warning. Prior to revision 5c5b5c7f1157,
that warning was suppressed (as it should be), but that is no longer
the case.

I suppose that fixing this would require modifying the function
package to set the "context visibility flag" correctly, but I don't
know how to do that -- hopefully someone else does?

- Brian