src/Pure/term.ML
changeset 18927 2e5b0f3f1418
parent 18893 2dbf73278b0e
child 18942 9228bbe9cd4e
     1.1 --- a/src/Pure/term.ML	Mon Feb 06 11:00:06 2006 +0100
     1.2 +++ b/src/Pure/term.ML	Mon Feb 06 11:00:24 2006 +0100
     1.3 @@ -56,6 +56,7 @@
     1.4    val fastype_of1: typ list * term -> typ
     1.5    val fastype_of: term -> typ
     1.6    val list_abs: (string * typ) list * term -> term
     1.7 +  val strip_abs: term -> (string * typ) list * term
     1.8    val strip_abs_body: term -> term
     1.9    val strip_abs_vars: term -> (string * typ) list
    1.10    val strip_qnt_body: string -> term -> term
    1.11 @@ -69,11 +70,11 @@
    1.12    val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
    1.13    val map_type_tfree: (string * sort -> typ) -> typ -> typ
    1.14    val map_term_types: (typ -> typ) -> term -> term
    1.15 -  val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
    1.16    val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
    1.17    val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
    1.18    val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
    1.19    val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
    1.20 +  val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
    1.21    val add_term_names: term * string list -> string list
    1.22    val add_term_varnames: term -> indexname list -> indexname list
    1.23    val term_varnames: term -> indexname list
    1.24 @@ -391,6 +392,11 @@
    1.25  
    1.26  val list_abs = Library.foldr (fn ((x, T), t) => Abs (x, T, t));
    1.27  
    1.28 +fun strip_abs (Abs (a, T, t)) =
    1.29 +      let val (a', t') = strip_abs t
    1.30 +      in ((a, T) :: a', t') end
    1.31 +  | strip_abs t = ([], t);
    1.32 +
    1.33  (* maps  (x1,...,xn)t   to   t  *)
    1.34  fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t
    1.35    | strip_abs_body u  =  u;