revert making 'map_cong' a 'cong' -- it breaks too many proofs in the AFP

--- 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:] ~ \\

--- 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], []),