1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
     1.3 @@ -485,19 +485,24 @@
     1.4              val rec_tacss =
     1.5                map2 (map o mk_iter_like_tac pre_map_defs rec_defs) fp_rec_thms ctr_defss;
     1.6            in
     1.7 +            ([], [])
     1.8 +(* NOTYET
     1.9              (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
    1.10                 goal_iterss iter_tacss,
    1.11               map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
    1.12                 goal_recss rec_tacss)
    1.13 +*)
    1.14            end;
    1.15  
    1.16 -        val notes =
    1.17 +        val notes = [];
    1.18 +(* NOTYET
    1.19            [(itersN, iter_thmss),
    1.20             (recsN, rec_thmss)]
    1.21            |> maps (fn (thmN, thmss) =>
    1.22              map2 (fn b => fn thms =>
    1.23                  ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    1.24                bs thmss);
    1.25 +*)
    1.26        in
    1.27          lthy |> Local_Theory.notes notes |> snd
    1.28        end;

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     2.3 @@ -53,10 +53,9 @@
     2.4  val iter_like_thms =
     2.5    @{thms case_unit comp_def convol_def id_def map_pair_def sum.simps(5,6) sum_map.simps split_conv};
     2.6  
     2.7 -fun mk_iter_like_tac iter_like_defs fld_iter_likes ctr_def pre_map_def ctxt =
     2.8 -  Local_Defs.unfold_tac ctxt (ctr_def :: pre_map_def :: iter_like_defs @ fld_iter_likes) THEN
     2.9 -  Local_Defs.unfold_tac ctxt iter_like_thms THEN
    2.10 -  rtac refl 1;
    2.11 +fun mk_iter_like_tac map_defs iter_like_defs fld_iter_like ctr_def ctxt =
    2.12 +  Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ map_defs) THEN
    2.13 +  Local_Defs.unfold_tac ctxt iter_like_thms THEN rtac refl 1;
    2.14  
    2.15  val coiter_like_ss = ss_only @{thms if_True if_False};
    2.16  val coiter_like_thms = @{thms id_def map_pair_def sum_map.simps prod.cases};

     3.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:04:26 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:04:26 2012 +0200
     3.3 @@ -134,6 +134,9 @@
     3.4      ((name, Typedef.transform_info phi info), lthy)
     3.5    end;
     3.6  
     3.7 +val pre_N = "pre_"
     3.8 +val raw_N = "raw_"
     3.9 +
    3.10  val coN = "co"
    3.11  val algN = "alg"
    3.12  val IITN = "IITN"
    3.13 @@ -299,7 +302,7 @@
    3.14      val Dss = map3 (append oo map o nth) livess kill_poss deadss;
    3.15  
    3.16      val ((bnfs'', deadss), lthy'') =
    3.17 -      fold_map3 (seal_bnf unfold') (map (Binding.suffix_name "BNF") bs) Dss bnfs' lthy'
    3.18 +      fold_map3 (seal_bnf unfold') (map (Binding.prefix_name pre_N) bs) Dss bnfs' lthy'
    3.19        |>> split_list;
    3.20  
    3.21      val pre_map_defs = map map_def_of_bnf bnfs'';
    3.22 @@ -319,7 +322,7 @@
    3.23      val (lhss, rhss) = split_list eqs;
    3.24      val sort = fp_sort lhss (SOME resBs);
    3.25      val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
    3.26 -      (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort) bs rhss
    3.27 +      (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.prefix_name raw_N b) I sort) bs rhss
    3.28          (empty_unfold, lthy));
    3.29    in
    3.30      mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold lthy'
    3.31 @@ -332,7 +335,7 @@
    3.32      val sort = fp_sort lhss NONE;
    3.33      val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
    3.34        (fold_map2 (fn b => fn rawT =>
    3.35 -        (bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort (Syntax.read_typ lthy rawT)))
    3.36 +        (bnf_of_typ Smart_Inline (Binding.prefix_name raw_N b) I sort (Syntax.read_typ lthy rawT)))
    3.37        bs raw_bnfs (empty_unfold, lthy));
    3.38    in
    3.39      snd (mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy')