# HG changeset patch
# User blanchet
# Date 1347132795 -7200
# Node ID f43d28683679d95f9f95d0f435d51411236c14de
# Parent  cbe8c859817c4b8fc0f796c325a1e297e3da3edf
tuning

diff -r cbe8c859817c -r f43d28683679 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:30:31 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:33:15 2012 +0200
@@ -138,8 +138,8 @@
     ((name, Typedef.transform_info phi info), lthy)
   end;
 
-val pre_N = "pre_"
-val raw_N = "raw_"
+val preN = "pre_"
+val rawN = "raw_"
 
 val coN = "co"
 val algN = "alg"
@@ -310,7 +310,7 @@
     val Dss = map3 (append oo map o nth) livess kill_poss deadss;
 
     val ((bnfs'', deadss), lthy'') =
-      fold_map3 (seal_bnf unfold') (map (Binding.prefix_name pre_N) bs) Dss bnfs' lthy'
+      fold_map3 (seal_bnf unfold') (map (Binding.prefix_name preN) bs) Dss bnfs' lthy'
       |>> split_list;
 
     val pre_map_defs = map map_def_of_bnf bnfs'';
@@ -330,7 +330,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.prefix_name raw_N b) I sort) bs rhss
+      (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.prefix_name rawN 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'
@@ -343,7 +343,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.prefix_name raw_N b) I sort (Syntax.read_typ lthy rawT)))
+        (bnf_of_typ Smart_Inline (Binding.prefix_name rawN 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')
diff -r cbe8c859817c -r f43d28683679 src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Sat Sep 08 21:30:31 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Sat Sep 08 21:33:15 2012 +0200
@@ -20,10 +20,10 @@
 open BNF_Util
 open BNF_Wrap_Tactics
 
-val is_N = "is_";
-val un_N = "un_";
-fun mk_un_N 1 1 suf = un_N ^ suf
-  | mk_un_N _ l suf = un_N ^ suf ^ string_of_int l;
+val isN = "is_";
+val unN = "un_";
+fun mk_unN 1 1 suf = unN ^ suf
+  | mk_unN _ l suf = unN ^ suf ^ string_of_int l;
 
 val case_congN = "case_cong";
 val case_eqN = "case_eq";
@@ -107,7 +107,7 @@
     fun can_omit_disc_binder k m =
       n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k));
 
-    val fallback_disc_binder = Binding.name o prefix is_N o Long_Name.base_name o name_of_ctr;
+    val fallback_disc_binder = Binding.name o prefix isN o Long_Name.base_name o name_of_ctr;
 
     val disc_binders =
       raw_disc_binders'
@@ -122,7 +122,7 @@
     val no_discs = map is_none disc_binders;
     val no_discs_at_all = forall I no_discs;
 
-    fun fallback_sel_binder m l = Binding.name o mk_un_N m l o Long_Name.base_name o name_of_ctr;
+    fun fallback_sel_binder m l = Binding.name o mk_unN m l o Long_Name.base_name o name_of_ctr;
 
     val sel_binderss =
       pad_list [] n raw_sel_binderss