# 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