# HG changeset patch
# User blanchet
# Date 1347131066 -7200
# Node ID d01a5c918298acab5c709cc366112931963e1a36
# Parent  0c9546fc789fb9e725b72a5673b5b51c2fc3922a
renamed xxxBNF to pre_xxx

diff -r 0c9546fc789f -r d01a5c918298 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -485,19 +485,24 @@
             val rec_tacss =
               map2 (map o mk_iter_like_tac pre_map_defs rec_defs) fp_rec_thms ctr_defss;
           in
+            ([], [])
+(* NOTYET
             (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
                goal_iterss iter_tacss,
              map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
                goal_recss rec_tacss)
+*)
           end;
 
-        val notes =
+        val notes = [];
+(* NOTYET
           [(itersN, iter_thmss),
            (recsN, rec_thmss)]
           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>
                 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
               bs thmss);
+*)
       in
         lthy |> Local_Theory.notes notes |> snd
       end;
diff -r 0c9546fc789f -r d01a5c918298 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -53,10 +53,9 @@
 val iter_like_thms =
   @{thms case_unit comp_def convol_def id_def map_pair_def sum.simps(5,6) sum_map.simps split_conv};
 
-fun mk_iter_like_tac iter_like_defs fld_iter_likes ctr_def pre_map_def ctxt =
-  Local_Defs.unfold_tac ctxt (ctr_def :: pre_map_def :: iter_like_defs @ fld_iter_likes) THEN
-  Local_Defs.unfold_tac ctxt iter_like_thms THEN
-  rtac refl 1;
+fun mk_iter_like_tac map_defs iter_like_defs fld_iter_like ctr_def ctxt =
+  Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ map_defs) THEN
+  Local_Defs.unfold_tac ctxt iter_like_thms THEN rtac refl 1;
 
 val coiter_like_ss = ss_only @{thms if_True if_False};
 val coiter_like_thms = @{thms id_def map_pair_def sum_map.simps prod.cases};
diff -r 0c9546fc789f -r d01a5c918298 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -134,6 +134,9 @@
     ((name, Typedef.transform_info phi info), lthy)
   end;
 
+val pre_N = "pre_"
+val raw_N = "raw_"
+
 val coN = "co"
 val algN = "alg"
 val IITN = "IITN"
@@ -299,7 +302,7 @@
     val Dss = map3 (append oo map o nth) livess kill_poss deadss;
 
     val ((bnfs'', deadss), lthy'') =
-      fold_map3 (seal_bnf unfold') (map (Binding.suffix_name "BNF") bs) Dss bnfs' lthy'
+      fold_map3 (seal_bnf unfold') (map (Binding.prefix_name pre_N) bs) Dss bnfs' lthy'
       |>> split_list;
 
     val pre_map_defs = map map_def_of_bnf bnfs'';
@@ -319,7 +322,7 @@
     val (lhss, rhss) = split_list eqs;
     val sort = fp_sort lhss (SOME resBs);
     val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
-      (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort) bs rhss
+      (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.prefix_name raw_N b) I sort) bs rhss
         (empty_unfold, lthy));
   in
     mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold lthy'
@@ -332,7 +335,7 @@
     val sort = fp_sort lhss NONE;
     val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
       (fold_map2 (fn b => fn rawT =>
-        (bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort (Syntax.read_typ lthy rawT)))
+        (bnf_of_typ Smart_Inline (Binding.prefix_name raw_N b) I sort (Syntax.read_typ lthy rawT)))
       bs raw_bnfs (empty_unfold, lthy));
   in
     snd (mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy')