--- 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;