# HG changeset patch
# User blanchet
# Date 1366815823 -7200
# Node ID 224b6eb2313a6ff2e0eb081498623aad6e10a13f
# Parent  67f05cb13e08545facc3bf433646592bd9f284a6
added "fundef_cong" attribute to "map_cong"

diff -r 67f05cb13e08 -r 224b6eb2313a src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 16:43:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 17:03:43 2013 +0200
@@ -105,6 +105,8 @@
 open BNF_Tactics
 open BNF_Def_Tactics
 
+val fundef_cong_attrs = @{attributes [fundef_cong]};
+
 type axioms = {
   map_id: thm,
   map_comp: thm,
@@ -1219,24 +1221,24 @@
           |> (if fact_policy <> Dont_Note then
                 let
                   val notes =
-                    [(map_comp'N, [Lazy.force (#map_comp' facts)]),
-                    (map_cong0N, [#map_cong0 axioms]),
-                    (map_congN, [Lazy.force (#map_cong facts)]),
-                    (map_id'N, [Lazy.force (#map_id' facts)]),
-                    (rel_eqN, [Lazy.force (#rel_eq facts)]),
-                    (rel_flipN, [Lazy.force (#rel_flip facts)]),
-                    (rel_srelN, [Lazy.force (#rel_srel facts)]),
-                    (set_natural'N, map Lazy.force (#set_natural' facts)),
-                    (srel_O_GrN, srel_O_Grs),
-                    (srel_IdN, [Lazy.force (#srel_Id facts)]),
-                    (srel_GrN, [Lazy.force (#srel_Gr facts)]),
-                    (srel_converseN, [Lazy.force (#srel_converse facts)]),
-                    (srel_monoN, [Lazy.force (#srel_mono facts)]),
-                    (srel_ON, [Lazy.force (#srel_O facts)])]
+                    [(map_comp'N, [Lazy.force (#map_comp' facts)], []),
+                    (map_cong0N, [#map_cong0 axioms], []),
+                    (map_congN, [Lazy.force (#map_cong facts)], fundef_cong_attrs),
+                    (map_id'N, [Lazy.force (#map_id' facts)], []),
+                    (rel_eqN, [Lazy.force (#rel_eq facts)], []),
+                    (rel_flipN, [Lazy.force (#rel_flip facts)], []),
+                    (rel_srelN, [Lazy.force (#rel_srel facts)], []),
+                    (set_natural'N, map Lazy.force (#set_natural' facts), []),
+                    (srel_O_GrN, srel_O_Grs, []),
+                    (srel_IdN, [Lazy.force (#srel_Id facts)], []),
+                    (srel_GrN, [Lazy.force (#srel_Gr facts)], []),
+                    (srel_converseN, [Lazy.force (#srel_converse facts)], []),
+                    (srel_monoN, [Lazy.force (#srel_mono facts)], []),
+                    (srel_ON, [Lazy.force (#srel_O facts)], [])]
                     |> filter_out (null o #2)
-                    |> map (fn (thmN, thms) =>
-                      ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []),
-                      [(thms, [])]));
+                    |> map (fn (thmN, thms, attrs) =>
+                      ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)),
+                        attrs), [(thms, [])]));
                 in
                   Local_Theory.notes notes #> snd
                 end