# HG changeset patch
# User blanchet
# Date 1382299148 -7200
# Node ID c0b0e1ea839e503f8fa756a2439b35ec1e9d8f9a
# Parent  402fcacb5c8893ef7513afde7ba795f32d23a5ef
tuning

diff -r 402fcacb5c88 -r c0b0e1ea839e src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sun Oct 20 19:23:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sun Oct 20 21:59:08 2013 +0200
@@ -232,6 +232,9 @@
   | flat_corec_preds_predsss_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) =
     p :: flat_corec_predss_getterss qss fss @ flat_corec_preds_predsss_gettersss ps qsss fsss;
 
+fun mk_tupled_fun x f xs =
+  if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs));
+
 fun mk_uncurried2_fun f xss =
   mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat_rec_arg_args xss);
 
diff -r 402fcacb5c88 -r c0b0e1ea839e src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Sun Oct 20 19:23:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Sun Oct 20 21:59:08 2013 +0200
@@ -139,7 +139,6 @@
   val mk_sumTN_balanced: typ list -> typ
 
   val mk_convol: term * term -> term
-  val mk_tupled_fun: term -> term -> term list -> term
 
   val Inl_const: typ -> typ -> term
   val Inr_const: typ -> typ -> term
@@ -382,9 +381,6 @@
     val convolT = fTU --> gTU --> gT --> HOLogic.mk_prodT (fU, gU);
   in Const (@{const_name convol}, convolT) $ f $ g end;
 
-fun mk_tupled_fun x f xs =
-  if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs));
-
 fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
 fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;