diff -r 4227b1510552 -r 2e5b0f3f1418 src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Feb 06 11:00:06 2006 +0100
+++ b/src/Pure/term.ML	Mon Feb 06 11:00:24 2006 +0100
@@ -56,6 +56,7 @@
   val fastype_of1: typ list * term -> typ
   val fastype_of: term -> typ
   val list_abs: (string * typ) list * term -> term
+  val strip_abs: term -> (string * typ) list * term
   val strip_abs_body: term -> term
   val strip_abs_vars: term -> (string * typ) list
   val strip_qnt_body: string -> term -> term
@@ -69,11 +70,11 @@
   val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
   val map_type_tfree: (string * sort -> typ) -> typ -> typ
   val map_term_types: (typ -> typ) -> term -> term
-  val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
   val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
   val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
   val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
   val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
+  val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
   val add_term_names: term * string list -> string list
   val add_term_varnames: term -> indexname list -> indexname list
   val term_varnames: term -> indexname list
@@ -391,6 +392,11 @@
 
 val list_abs = Library.foldr (fn ((x, T), t) => Abs (x, T, t));
 
+fun strip_abs (Abs (a, T, t)) =
+      let val (a', t') = strip_abs t
+      in ((a, T) :: a', t') end
+  | strip_abs t = ([], t);
+
 (* maps  (x1,...,xn)t   to   t  *)
 fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t
   | strip_abs_body u  =  u;