1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -206,6 +206,7 @@
     1.4  val id_def = @{thm id_def};
     1.5  val mp_conj = @{thm mp_conj};
     1.6  
     1.7 +val fundefcong_attrs = @{attributes [fundef_cong]};
     1.8  val nitpicksimp_attrs = @{attributes [nitpick_simp]};
     1.9  val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
    1.10  val simp_attrs = @{attributes [simp]};
    1.11 @@ -220,9 +221,7 @@
    1.12  fun flat_rec_arg_args xss =
    1.13    (* FIXME (once the old datatype package is phased out): The first line below gives the preferred
    1.14       order. The second line is for compatibility with the old datatype package. *)
    1.15 -(*
    1.16 -  flat xss
    1.17 -*)
    1.18 +  (* flat xss *)
    1.19    map hd xss @ maps tl xss;
    1.20  
    1.21  fun flat_corec_predss_getterss qss fss = maps (op @) (qss ~~ fss);
    1.22 @@ -1248,7 +1247,7 @@
    1.23                (sel_bindingss, sel_defaultss))) lthy
    1.24            end;
    1.25  
    1.26 -        fun derive_maps_sets_rels (ctr_sugar, lthy) =
    1.27 +        fun derive_maps_sets_rels (ctr_sugar as {case_cong, ...} : ctr_sugar, lthy) =
    1.28            if live = 0 then
    1.29              ((([], [], [], []), ctr_sugar), lthy)
    1.30            else
    1.31 @@ -1322,7 +1321,8 @@
    1.32                  join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
    1.33  
    1.34                val anonymous_notes =
    1.35 -                [(map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms,
    1.36 +                [([case_cong], fundefcong_attrs),
    1.37 +                 (map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms,
    1.38                    code_nitpicksimp_attrs),
    1.39                   (map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
    1.40                      rel_inject_thms ms, code_nitpicksimp_attrs)]