# HG changeset patch
# User blanchet
# Date 1367937797 -7200
# Node ID 2891ee28f550913aab3b2347b07a5ada6dadc45a
# Parent  ba735ac9044ae3c254bf9a219527bb7ad09028cb
tuning

diff -r ba735ac9044a -r 2891ee28f550 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 16:18:42 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 16:43:17 2013 +0200
@@ -241,10 +241,8 @@
     if exists_subtype_in fpTs T then ([project_recT fst T], [project_recT snd T]) else ([T], [])
   end;
 
-val massage_rec_fun_arg_typesss = map o map o flat_rec o unzip_recT;
-
 fun mk_fold_fun_typess y_Tsss Cs = map2 (fn C => map (fn y_Ts => y_Ts ---> C)) Cs y_Tsss;
-val mk_rec_fun_typess = mk_fold_fun_typess oo massage_rec_fun_arg_typesss;
+val mk_rec_fun_typess = mk_fold_fun_typess oo map o map o flat_rec o unzip_recT;
 
 fun mk_fun_arg_typess n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;