# HG changeset patch
# User blanchet
# Date 1369660414 -7200
# Node ID ec337c3438a77a605c95e62ead71794864289f1e
# Parent  1b3f907caf614691456a73c020c5627f10c8ae4e
tuning

diff -r 1b3f907caf61 -r ec337c3438a7 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon May 27 15:00:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon May 27 15:13:34 2013 +0200
@@ -243,10 +243,6 @@
 
 val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of;
 
-fun mk_fp_iters thy lfp fpTs Cs fp_iters0 =
-  mk_co_iters thy lfp fpTs Cs fp_iters0
-  |> `(mk_fp_iter_fun_types o hd);
-
 fun unzip_recT fpTs T =
   let
     fun project_recT proj =
@@ -355,8 +351,10 @@
   let
     val thy = Proof_Context.theory_of lthy;
 
-    val (fp_fold_fun_Ts, fp_folds) = mk_fp_iters thy lfp fpTs Cs fp_folds0;
-    val (fp_rec_fun_Ts, fp_recs) = mk_fp_iters thy lfp fpTs Cs fp_recs0;
+    val (fp_fold_fun_Ts, fp_folds) = mk_co_iters thy lfp fpTs Cs fp_folds0
+      |> `(mk_fp_iter_fun_types o hd);
+    val (fp_rec_fun_Ts, fp_recs) = mk_co_iters thy lfp fpTs Cs fp_recs0
+      |> `(mk_fp_iter_fun_types o hd);
 
     val ((fold_rec_args_types, unfold_corec_args_types), lthy') =
       if lfp then