1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 11 23:27:19 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 00:20:37 2012 +0200
     1.3 @@ -34,6 +34,8 @@
     1.4  val sel_coitersN = "sel_coiters";
     1.5  val sel_corecsN = "sel_corecs";
     1.6  
     1.7 +val simp_attrs = @{attributes [simp]};
     1.8 +
     1.9  fun split_list11 xs =
    1.10    (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs,
    1.11     map #9 xs, map #10 xs, map #11 xs);
    1.12 @@ -424,12 +426,14 @@
    1.13                        map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss));
    1.14                in (binder, spec) end;
    1.15  
    1.16 -            val iter_like_bundles =
    1.17 +            val iter_like_infos =
    1.18                [(iterN, fp_iter, iter_only),
    1.19                 (recN, fp_rec, rec_only)];
    1.20  
    1.21 -            val (binders, specs) = map generate_iter_like iter_like_bundles |> split_list;
    1.22 +            val (binders, specs) = map generate_iter_like iter_like_infos |> split_list;
    1.23  
    1.24 +            (* TODO: Allow same constructor (and selector/discriminator) names for different
    1.25 +               types (cf. old "datatype" package) *)
    1.26              val ((csts, defs), (lthy', lthy)) = no_defs_lthy
    1.27                |> apfst split_list o fold_map2 (fn b => fn spec =>
    1.28                  Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec))
    1.29 @@ -468,11 +472,11 @@
    1.30                        map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss));
    1.31                in (binder, spec) end;
    1.32  
    1.33 -            val coiter_like_bundles =
    1.34 +            val coiter_like_infos =
    1.35                [(coiterN, fp_iter, coiter_only),
    1.36                 (corecN, fp_rec, corec_only)];
    1.37  
    1.38 -            val (binders, specs) = map generate_coiter_like coiter_like_bundles |> split_list;
    1.39 +            val (binders, specs) = map generate_coiter_like coiter_like_infos |> split_list;
    1.40  
    1.41              val ((csts, defs), (lthy', lthy)) = no_defs_lthy
    1.42                |> apfst split_list o fold_map2 (fn b => fn spec =>
    1.43 @@ -569,12 +573,12 @@
    1.44            end;
    1.45  
    1.46          val notes =
    1.47 -          [(itersN, iter_thmss),
    1.48 -           (recsN, rec_thmss)]
    1.49 -          |> maps (fn (thmN, thmss) =>
    1.50 +          [(itersN, iter_thmss, simp_attrs),
    1.51 +           (recsN, rec_thmss, Code.add_default_eqn_attrib :: simp_attrs)]
    1.52 +          |> maps (fn (thmN, thmss, attrs) =>
    1.53              map2 (fn b => fn thms =>
    1.54 -                ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    1.55 -              bs thmss);
    1.56 +              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
    1.57 +                [(thms, [])])) bs thmss);
    1.58        in
    1.59          lthy |> Local_Theory.notes notes |> snd
    1.60        end;
    1.61 @@ -663,15 +667,15 @@
    1.62            map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss sel_thmsss;
    1.63  
    1.64          val notes =
    1.65 -          [(coitersN, coiter_thmss),
    1.66 -           (disc_coitersN, disc_coiter_thmss),
    1.67 -           (sel_coitersN, map flat sel_coiter_thmsss),
    1.68 -           (corecsN, corec_thmss),
    1.69 -           (disc_corecsN, disc_corec_thmss),
    1.70 -           (sel_corecsN, map flat sel_corec_thmsss)]
    1.71 -          |> maps (fn (thmN, thmss) =>
    1.72 +          [(coitersN, coiter_thmss, []),
    1.73 +           (disc_coitersN, disc_coiter_thmss, []),
    1.74 +           (sel_coitersN, map flat sel_coiter_thmsss, []),
    1.75 +           (corecsN, corec_thmss, []),
    1.76 +           (disc_corecsN, disc_corec_thmss, []),
    1.77 +           (sel_corecsN, map flat sel_corec_thmsss, [])]
    1.78 +          |> maps (fn (thmN, thmss, attrs) =>
    1.79              map_filter (fn (_, []) => NONE | (b, thms) =>
    1.80 -              SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []),
    1.81 +              SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
    1.82                  [(thms, [])])) (bs ~~ thmss));
    1.83        in
    1.84          lthy |> Local_Theory.notes notes |> snd