--- a/src/Pure/term.ML Fri Sep 21 22:51:10 2007 +0200
+++ b/src/Pure/term.ML Fri Sep 21 22:51:12 2007 +0200
@@ -183,6 +183,7 @@
val maxidx_typ: typ -> int -> int
val maxidx_typs: typ list -> int -> int
val maxidx_term: term -> int -> int
+ val has_abs: term -> bool
val dest_abs: string * typ * term -> string * term
val declare_term_names: term -> Name.context -> Name.context
val variant_frees: term -> (string * 'a) list -> (string * 'a) list
@@ -1103,6 +1104,11 @@
| _ => false);
in ex end;
+fun has_abs (Abs _) = true
+ | has_abs (t $ u) = has_abs t orelse has_abs u
+ | has_abs _ = false;
+
+
(** Consts etc. **)