tuning

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 19 17:16:40 2014 +1100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 19 08:33:59 2014 +0100
@@ -342,7 +342,7 @@
 fun mk_iters_args_types ctr_Tsss Cs ns mss ctor_iter_fun_Tss lthy =
   let
     val Css = map2 replicate ns Cs;
-    val y_Tsss = map3 mk_iter_fun_arg_types0 ns mss (map un_fold_of ctor_iter_fun_Tss);
+    val y_Tsss = map3 mk_iter_fun_arg_types ns mss (map un_fold_of ctor_iter_fun_Tss);
     val g_Tss = map2 (fn C => map (fn y_Ts => y_Ts ---> C)) Cs y_Tsss;
 
     val ((gss, ysss), lthy) =

--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Wed Feb 19 17:16:40 2014 +1100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Wed Feb 19 08:33:59 2014 +0100
@@ -21,11 +21,9 @@
 
   val get_free_indices: ((binding * typ) * 'a) list -> term -> int list
 
-  (* needed here for bootstrapping; would be more at home in "bnf_fp_def_sugar.ML" *)
+  (* needed here for bootstrapping; would be more at home in "bnf_fp_def_sugar.ML" (FIXME) *)
   val unzip_recT: typ -> typ -> typ list
-  val mk_iter_fun_arg_types0: int -> int list -> typ -> typ list list
-  val mk_iter_fun_arg_types: typ list list list -> int list -> int list list -> typ ->
-    typ list list list list
+  val mk_iter_fun_arg_types: int -> int list -> typ -> typ list list
   val flat_rec_arg_args: 'a list list -> 'a list
   val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term
 end;
@@ -61,12 +59,7 @@
   | unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts
   | unzip_recT _ T = [T];
 
-fun mk_iter_fun_arg_types0 n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
-
-fun mk_iter_fun_arg_types ctr_Tsss ns mss =
-  binder_fun_types
-  #> map3 mk_iter_fun_arg_types0 ns mss
-  #> map2 (map2 (map2 unzip_recT)) ctr_Tsss;
+fun mk_iter_fun_arg_types n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
 
 fun flat_rec_arg_args xss =
   (* FIXME (once the old datatype package is phased out): The first line below gives the preferred

--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Feb 19 17:16:40 2014 +1100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Feb 19 08:33:59 2014 +0100
@@ -146,7 +146,9 @@
     val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss;
     val perm_Cs = map (body_type o #ctor_recT) perm_basic_lfp_sugars;
     val perm_fun_arg_Tssss =
-      mk_iter_fun_arg_types perm_ctr_Tsss perm_ns perm_mss (#ctor_recT (hd perm_basic_lfp_sugars));
+      binder_fun_types (#ctor_recT (hd perm_basic_lfp_sugars))
+      |> map3 mk_iter_fun_arg_types perm_ns perm_mss
+      |> map2 (map2 (map2 unzip_recT)) perm_ctr_Tsss;
 
     fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs;
     fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs;

--- a/src/HOL/Tools/BNF/bnf_util.ML	Wed Feb 19 17:16:40 2014 +1100
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Wed Feb 19 08:33:59 2014 +0100
@@ -326,9 +326,8 @@
 (** Types **)
 
 (*stolen from ~~/src/HOL/Tools/Nitpick/nitpick_hol.ML*)
-fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
-    1 + num_binder_types T2
-  | num_binder_types _ = 0
+fun num_binder_types (Type (@{type_name fun}, [_, T])) = 1 + num_binder_types T
+  | num_binder_types _ = 0;
 
 (*maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T)*)
 fun strip_typeN 0 T = ([], T)
@@ -393,8 +392,7 @@
 
 fun mk_image f =
   let val (T, U) = dest_funT (fastype_of f);
-  in Const (@{const_name image},
-    (T --> U) --> (HOLogic.mk_setT T) --> (HOLogic.mk_setT U)) $ f end;
+  in Const (@{const_name image}, (T --> U) --> HOLogic.mk_setT T --> HOLogic.mk_setT U) $ f end;
 
 fun mk_Ball X f =
   Const (@{const_name Ball}, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f;
@@ -431,8 +429,7 @@
       mk_Field bd $ bd
   end;
 
-fun mk_cinfinite bd =
-  Const (@{const_name cinfinite}, fastype_of bd --> HOLogic.boolT) $ bd;
+fun mk_cinfinite bd = Const (@{const_name cinfinite}, fastype_of bd --> HOLogic.boolT) $ bd;
 
 fun mk_ordLeq t1 t2 =
   HOLogic.mk_mem (HOLogic.mk_prod (t1, t2),
@@ -477,9 +474,7 @@
   let
     val (T1, relT1) = `(fst o dest_relT) (fastype_of t1);
     val (T2, relT2) = `(fst o dest_relT) (fastype_of t2);
-  in
-    Const (binop, relT1 --> relT2 --> mk_relT (typop (T1, T2), typop (T1, T2))) $ t1 $ t2
-  end;
+  in Const (binop, relT1 --> relT2 --> mk_relT (typop (T1, T2), typop (T1, T2))) $ t1 $ t2 end;
 
 val mk_csum = mk_card_binop @{const_name csum} mk_sumT;
 val mk_cprod = mk_card_binop @{const_name cprod} HOLogic.mk_prodT;