--- a/src/Pure/term.ML Tue Mar 11 17:20:59 1997 +0100
+++ b/src/Pure/term.ML Fri Mar 14 10:35:30 1997 +0100
@@ -283,6 +283,10 @@
| loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
| loose_bvar _ = false;
+fun loose_bvar1(Bound i,k) = i = k
+ | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
+ | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
+ | loose_bvar1 _ = false;
(*Substitute arguments for loose bound variables.
Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).