added has_abs (from envir.ML);
authorwenzelm
Fri Sep 21 22:51:12 2007 +0200 (2007-09-21)
changeset 2467135075a1e9599
parent 24670 9aae962b1d56
child 24672 f311717d1f03
added has_abs (from envir.ML);
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Fri Sep 21 22:51:10 2007 +0200
     1.2 +++ b/src/Pure/term.ML	Fri Sep 21 22:51:12 2007 +0200
     1.3 @@ -183,6 +183,7 @@
     1.4    val maxidx_typ: typ -> int -> int
     1.5    val maxidx_typs: typ list -> int -> int
     1.6    val maxidx_term: term -> int -> int
     1.7 +  val has_abs: term -> bool
     1.8    val dest_abs: string * typ * term -> string * term
     1.9    val declare_term_names: term -> Name.context -> Name.context
    1.10    val variant_frees: term -> (string * 'a) list -> (string * 'a) list
    1.11 @@ -1103,6 +1104,11 @@
    1.12        | _ => false);
    1.13    in ex end;
    1.14  
    1.15 +fun has_abs (Abs _) = true
    1.16 +  | has_abs (t $ u) = has_abs t orelse has_abs u
    1.17 +  | has_abs _ = false;
    1.18 +
    1.19 +
    1.20  
    1.21  (** Consts etc. **)
    1.22