# HG changeset patch
# User blanchet
# Date 1386012714 -3600
# Node ID 36301c99ed2613899e678b8dad1dc46153f5371b
# Parent  59388c359decbe3e389001616ba74e007b220f0a
revert making 'map_cong' a 'cong' -- it breaks too many proofs in the AFP

diff -r 59388c359dec -r 36301c99ed26 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Dec 02 20:31:54 2013 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Dec 02 20:31:54 2013 +0100
@@ -866,7 +866,7 @@
 \item[@{text "t."}\hthm{map\_comp}\rm:] ~ \\
 @{thm list.map_cong0[no_vars]}
 
-\item[@{text "t."}\hthm{map\_cong} @{text "[cong, fundef_cong]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{map\_cong} @{text "[fundef_cong]"}\rm:] ~ \\
 @{thm list.map_cong[no_vars]}
 
 \item[@{text "t."}\hthm{map\_id}\rm:] ~ \\
diff -r 59388c359dec -r 36301c99ed26 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Mon Dec 02 20:31:54 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Mon Dec 02 20:31:54 2013 +0100
@@ -125,7 +125,7 @@
 open BNF_Tactics
 open BNF_Def_Tactics
 
-val cong_fundefcong_attrs = @{attributes [cong, fundef_cong]};
+val fundefcong_attrs = @{attributes [fundef_cong]};
 
 type axioms = {
   map_id0: thm,
@@ -636,7 +636,7 @@
           val notes =
             [(map_compN, [Lazy.force (#map_comp facts)], []),
             (map_cong0N, [#map_cong0 axioms], []),
-            (map_congN, [Lazy.force (#map_cong facts)], cong_fundefcong_attrs),
+            (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
             (map_idN, [Lazy.force (#map_id facts)], []),
             (rel_comppN, [Lazy.force (#rel_OO facts)], []),
             (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),