1.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Mon Dec 02 20:31:54 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Mon Dec 02 20:31:54 2013 +0100
     1.3 @@ -125,7 +125,7 @@
     1.4  open BNF_Tactics
     1.5  open BNF_Def_Tactics
     1.6  
     1.7 -val fundef_cong_attrs = @{attributes [fundef_cong]};
     1.8 +val cong_fundefcong_attrs = @{attributes [cong, fundef_cong]};
     1.9  
    1.10  type axioms = {
    1.11    map_id0: thm,
    1.12 @@ -636,7 +636,7 @@
    1.13            val notes =
    1.14              [(map_compN, [Lazy.force (#map_comp facts)], []),
    1.15              (map_cong0N, [#map_cong0 axioms], []),
    1.16 -            (map_congN, [Lazy.force (#map_cong facts)], fundef_cong_attrs),
    1.17 +            (map_congN, [Lazy.force (#map_cong facts)], cong_fundefcong_attrs),
    1.18              (map_idN, [Lazy.force (#map_id facts)], []),
    1.19              (rel_eqN, [Lazy.force (#rel_eq facts)], []),
    1.20              (rel_flipN, [Lazy.force (#rel_flip facts)], []),