--- a/src/Pure/term.ML Thu Mar 24 16:47:24 2011 +0100
+++ b/src/Pure/term.ML Thu Mar 24 16:56:19 2011 +0100
@@ -154,6 +154,8 @@
val match_bvars: (term * term) * (string * string) list -> (string * string) list
val map_abs_vars: (string -> string) -> term -> term
val rename_abs: term -> term -> term -> term option
+ val is_open: term -> bool
+ val is_dependent: term -> bool
val lambda_name: string * term -> term -> term
val close_schematic_term: term -> term
val maxidx_typ: typ -> int -> int
@@ -650,6 +652,9 @@
| loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
| loose_bvar1 _ = false;
+fun is_open t = loose_bvar (t, 0);
+fun is_dependent t = loose_bvar1 (t, 0);
+
(*Substitute arguments for loose bound variables.
Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0