# HG changeset patch
# User wenzelm
# Date 1190407872 -7200
# Node ID 35075a1e9599205c6c22a6e5b270af403406a60a
# Parent  9aae962b1d5675c4f0107e7f6255a665837ab7db
added has_abs (from envir.ML);

diff -r 9aae962b1d56 -r 35075a1e9599 src/Pure/term.ML
--- 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. **)