tuning

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Jun 05 12:51:16 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Jun 05 13:13:35 2013 +0200
@@ -31,7 +31,6 @@
   val flat_rec: 'a list list -> 'a list
   val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term
   val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
-  val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c
   val mk_un_fold_co_rec_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list ->
     int list list -> term list -> term list -> Proof.context ->
     (term list * term list
@@ -433,7 +432,7 @@
 fun nesty_bnfs ctxt ctr_Tsss Us =
   map_filter (bnf_of ctxt) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_Tsss []);
 
-fun indexify_fst xs f (x, y) = f (find_index (curry (op =) x) xs) (x, y);
+fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p;
 
 fun build_map lthy build_simple =
   let
@@ -674,15 +673,19 @@
           fold_rev (fold_rev Logic.all) (xs :: fss)
             (mk_Trueprop_eq (fiter $ xctr, Term.list_comb (f, fxs)));
 
-        fun tick u f = Term.lambda u (HOLogic.mk_prod (u, f $ u));
+        fun maybe_tick (T, U) u f =
+          if try (fst o HOLogic.dest_prodT) U = SOME T then
+            Term.lambda u (HOLogic.mk_prod (u, f $ u))
+          else
+            f;
 
-        fun unzip_iters fiters maybe_tick (x as Free (_, T)) Us =
+        fun unzip_iters tick fiters (x as Free (_, T)) =
           map (fn U => if U = T then x else
-            build_map lthy (indexify_fst fpTs (fn kk => fn _ =>
-              nth fiters kk |> length Us = 1 ? maybe_tick (nth us kk))) (T, U) $ x) Us;
+            build_map lthy (indexify fst fpTs (fn kk => fn TU =>
+              nth fiters kk |> maybe_tick TU (nth us kk))) (T, U) $ x);
 
-        val gxsss = map2 (map2 (flat_rec oo map2 (unzip_iters gfolds (K I)))) xsss y_Tssss;
-        val hxsss = map2 (map2 (flat_rec oo map2 (unzip_iters hrecs tick))) xsss z_Tssss;
+        val gxsss = map2 (map2 (flat_rec oo map2 (unzip_iters false gfolds))) xsss y_Tssss;
+        val hxsss = map2 (map2 (flat_rec oo map2 (unzip_iters true hrecs))) xsss z_Tssss;
 
         val fold_goalss = map5 (map4 o mk_goal gss) gfolds xctrss gss xsss gxsss;
         val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;
@@ -853,7 +856,7 @@
         fun intr_coiters fcoiters [] [cf] =
             let val T = fastype_of cf in
               if exists_subtype_in Cs T then
-                build_map lthy (indexify_fst Cs (K o nth fcoiters)) (T, mk_U T) $ cf
+                build_map lthy (indexify fst Cs (K o nth fcoiters)) (T, mk_U T) $ cf
               else
                 cf
             end