1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sun Oct 20 19:23:28 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sun Oct 20 21:59:08 2013 +0200
     1.3 @@ -232,6 +232,9 @@
     1.4    | flat_corec_preds_predsss_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) =
     1.5      p :: flat_corec_predss_getterss qss fss @ flat_corec_preds_predsss_gettersss ps qsss fsss;
     1.6  
     1.7 +fun mk_tupled_fun x f xs =
     1.8 +  if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs));
     1.9 +
    1.10  fun mk_uncurried2_fun f xss =
    1.11    mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat_rec_arg_args xss);
    1.12  

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Sun Oct 20 19:23:28 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Sun Oct 20 21:59:08 2013 +0200
     2.3 @@ -139,7 +139,6 @@
     2.4    val mk_sumTN_balanced: typ list -> typ
     2.5  
     2.6    val mk_convol: term * term -> term
     2.7 -  val mk_tupled_fun: term -> term -> term list -> term
     2.8  
     2.9    val Inl_const: typ -> typ -> term
    2.10    val Inr_const: typ -> typ -> term
    2.11 @@ -382,9 +381,6 @@
    2.12      val convolT = fTU --> gTU --> gT --> HOLogic.mk_prodT (fU, gU);
    2.13    in Const (@{const_name convol}, convolT) $ f $ g end;
    2.14  
    2.15 -fun mk_tupled_fun x f xs =
    2.16 -  if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs));
    2.17 -
    2.18  fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
    2.19  fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;
    2.20