# HG changeset patch
# User blanchet
# Date 1370424624 -7200
# Node ID 4a4da43e855ac189d4700766ac999905ce636958
# Parent  085771de5720784a9e2ede8df5b86f0918c0c22b
tuning

diff -r 085771de5720 -r 4a4da43e855a src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Jun 05 11:16:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Jun 05 11:30:24 2013 +0200
@@ -253,13 +253,6 @@
 
 val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of;
 
-fun meta_unzip_rec getT left right nested fpTs y =
-  let val T = getT y in
-    if member (op =) fpTs T then [left y, right y]
-    else if exists_subtype_in fpTs T then [nested y]
-    else [y]
-  end;
-
 fun project_co_recT special_Tname Cs proj =
   let
     fun project (Type (s, Ts as [T, U])) =
@@ -683,13 +676,16 @@
         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_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 unzip_iters fiters maybe_tick maybe_mk_prodT x =
+          let val Free (_, T) = x in
+            if member (op =) fpTs T then
+              [x, build_map lthy (indexify_fst fpTs (K o nth fiters)) (T, mk_U T) $ x]
+            else if exists_subtype_in fpTs T then
+              [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]
+            else
+              [x]
+          end;
 
         fun tick u f = Term.lambda u (HOLogic.mk_prod (u, f $ u));