--- a/src/HOL/Tools/Function/function_lib.ML Tue Sep 28 12:10:37 2010 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML Tue Sep 28 12:34:41 2010 +0200
@@ -18,17 +18,6 @@
fun plural sg pl [x] = sg
| plural sg pl _ = pl
-(* lambda-abstracts over an arbitrarily nested tuple
- ==> hologic.ML? *)
-fun tupled_lambda vars t =
- case vars of
- (Free v) => lambda (Free v) t
- | (Var v) => lambda (Var v) t
- | (Const (@{const_name Pair}, Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
- (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
- | _ => raise Match
-
-
fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
let
val (n, body) = Term.dest_abs a