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 _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
