--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Sat Sep 08 21:04:26 2012 +0200
@@ -91,8 +91,6 @@
val dest_sumTN: int -> typ -> typ list
val dest_tupleT: int -> typ -> typ list
- val mk_uncurried_fun: term -> term list -> term
-
val mk_Field: term -> term
val mk_union: term * term -> term
@@ -232,8 +230,6 @@
| dest_tupleT 1 T = [T]
| dest_tupleT n (Type (@{type_name prod}, [T, T'])) = T :: dest_tupleT (n - 1) T';
-fun mk_uncurried_fun f xs = HOLogic.tupled_lambda (HOLogic.mk_tuple xs) (Term.list_comb (f, xs));
-
fun mk_Field r =
let val T = fst (dest_relT (fastype_of r));
in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end;