1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon Dec 02 20:31:54 2013 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Dec 02 20:31:54 2013 +0100
     1.3 @@ -866,7 +866,7 @@
     1.4  \item[@{text "t."}\hthm{map\_comp}\rm:] ~ \\
     1.5  @{thm list.map_cong0[no_vars]}
     1.6  
     1.7 -\item[@{text "t."}\hthm{map\_cong} @{text "[cong, fundef_cong]"}\rm:] ~ \\
     1.8 +\item[@{text "t."}\hthm{map\_cong} @{text "[fundef_cong]"}\rm:] ~ \\
     1.9  @{thm list.map_cong[no_vars]}
    1.10  
    1.11  \item[@{text "t."}\hthm{map\_id}\rm:] ~ \\

     2.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Mon Dec 02 20:31:54 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Mon Dec 02 20:31:54 2013 +0100
     2.3 @@ -125,7 +125,7 @@
     2.4  open BNF_Tactics
     2.5  open BNF_Def_Tactics
     2.6  
     2.7 -val cong_fundefcong_attrs = @{attributes [cong, fundef_cong]};
     2.8 +val fundefcong_attrs = @{attributes [fundef_cong]};
     2.9  
    2.10  type axioms = {
    2.11    map_id0: thm,
    2.12 @@ -636,7 +636,7 @@
    2.13            val notes =
    2.14              [(map_compN, [Lazy.force (#map_comp facts)], []),
    2.15              (map_cong0N, [#map_cong0 axioms], []),
    2.16 -            (map_congN, [Lazy.force (#map_cong facts)], cong_fundefcong_attrs),
    2.17 +            (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
    2.18              (map_idN, [Lazy.force (#map_id facts)], []),
    2.19              (rel_comppN, [Lazy.force (#rel_OO facts)], []),
    2.20              (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),