tuning

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Feb 18 17:52:27 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Feb 18 17:52:28 2014 +0100
@@ -263,8 +263,7 @@
       end)
   end;
 
-(* TODO: needed? *)
-fun indexify_callsss (fp_sugar as {ctr_sugar = {ctrs, ...}, ...} : fp_sugar) callsss =
+fun indexify_callsss ctrs callsss =
   let
     fun indexify_ctr ctr =
       (case AList.lookup Term.aconv_untyped callsss ctr of
@@ -332,9 +331,9 @@
 
           fun fresh_tyargs () =
             let
-              (* The name "'z" is unlikely to clash with the context, yielding more cache hits. *)
+              (* The name "'zy" is unlikely to clash with the context, yielding more cache hits. *)
               val (gen_tyargs, lthy') =
-                variant_tfrees (replicate (length tyargs) "z") lthy
+                variant_tfrees (replicate (length tyargs) "zy") lthy
                 |>> map Logic.varifyT_global;
               val rho' = (gen_tyargs ~~ tyargs) @ rho;
             in
@@ -388,7 +387,7 @@
     val perm_callssss0 = permute callssss0;
     val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts;
 
-    val perm_callssss = map2 indexify_callsss perm_fp_sugars0 perm_callssss0;
+    val perm_callssss = map2 (indexify_callsss o #ctrs o #ctr_sugar) perm_fp_sugars0 perm_callssss0;
 
     val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
 

--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Feb 18 17:52:27 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Feb 18 17:52:28 2014 +0100
@@ -150,7 +150,7 @@
     val recs = map (fst o dest_Const o co_rec_of o #co_iters) fp_sugars;
     val rec_thms = maps (co_rec_of o #co_iter_thmss) fp_sugars;
 
-    fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar as {casex, exhaust, nchotomy, injects,
+    fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects,
         distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) =
       (T_name0,
        {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct,