# HG changeset patch
# User blanchet
# Date 1393847300 -3600
# Node ID 756275b550d9730107144a32b6fb9f9b0143e19c
# Parent  21d0b48a5fb5f19730ad26bec8d56f62b4eb900f
make 'diff_iff' a simp rule if available

diff -r 21d0b48a5fb5 -r 756275b550d9 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -1315,11 +1315,15 @@
 
         val common_name = mk_common_name fun_names;
 
+        val anonymous_notes =
+          [(flat disc_iff_or_disc_thmss, simp_attrs)]
+          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
+
         val notes =
           [(coinductN, map (if n2m then single else K []) coinduct_thms, []),
            (codeN, code_thmss, code_nitpicksimp_attrs),
            (ctrN, ctr_thmss, []),
-           (discN, disc_thmss, simp_attrs),
+           (discN, disc_thmss, []),
            (disc_iffN, disc_iff_thmss, []),
            (excludeN, exclude_thmss, []),
            (exhaustN, nontriv_exhaust_thmss, []),
@@ -1343,7 +1347,7 @@
         |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat sel_thmss)
         |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat ctr_thmss)
         |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat code_thmss)
-        |> Local_Theory.notes (notes @ common_notes)
+        |> Local_Theory.notes (anonymous_notes @ notes @ common_notes)
         |> snd
       end;