# HG changeset patch
# User blanchet
# Date 1367953786 -7200
# Node ID 31bb70ddee7e85d31be3204fabaa2624b99821bb
# Parent  eb3169abcbd5b0f958f13eb3fb9a7e8af2dd27ca
tuning

diff -r eb3169abcbd5 -r 31bb70ddee7e src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 18:40:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 21:09:46 2013 +0200
@@ -228,9 +228,8 @@
 
 val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of;
 
-fun mk_fp_iter lfp As Cs fp_iters0 =
-  map (mk_co_iter lfp As Cs) fp_iters0
-  |> (fn ts => (ts, mk_fp_iter_fun_types (hd ts)));
+fun mk_fp_iter lfp As Cs =
+  map (mk_co_iter lfp As Cs) #> (fn ts => (ts, mk_fp_iter_fun_types (hd ts)));
 
 fun unzip_recT fpTs T =
   let