tuning

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed May 29 02:35:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed May 29 03:10:26 2013 +0200
@@ -681,30 +681,15 @@
 
         val mk_U = typ_subst_nonatomic (map2 pair fpTs Cs);
 
-        (* ### *)
-        fun typ_subst inst (T as Type (s, Ts)) =
-            (case AList.lookup (op =) inst T of
-              NONE => Type (s, map (typ_subst inst) Ts)
-            | SOME T' => T')
-          | typ_subst inst T = the_default T (AList.lookup (op =) inst T);
-
-        fun mk_U' maybe_mk_prodT =
-          typ_subst (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs);
-
-        (* ### *)
-        fun build_rec_like fiters maybe_tick (T, U) =
-          if T = U then
-            id_const T
-          else
-            (case find_index (curry (op =) T) fpTs of
-              ~1 => build_map lthy (build_rec_like fiters maybe_tick) (T, U)
-            | kk => maybe_tick (nth us kk) (nth fiters kk));
+        fun mk_nested_U maybe_mk_prodT =
+          typ_subst_nonatomic (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs);
 
         fun unzip_iters fiters maybe_tick maybe_mk_prodT =
           meta_unzip_rec (snd o dest_Free) I
             (fn x as Free (_, T) => build_map lthy (indexify_fst fpTs (K o nth fiters))
               (T, mk_U T) $ x)
-            (fn x as Free (_, T) => build_rec_like fiters maybe_tick (T, mk_U' maybe_mk_prodT T) $ x)
+            (fn x as Free (_, T) => build_map lthy (indexify_fst fpTs (fn kk => fn _ =>
+              maybe_tick (nth us kk) (nth fiters kk))) (T, mk_nested_U maybe_mk_prodT T) $ x)
             fpTs;
 
         fun tick u f = Term.lambda u (HOLogic.mk_prod (u, f $ u));