src/Pure/term.ML
changeset 2792 6c17c5ec3d8b
parent 2752 74a9aead96c8
child 2959 071bfb16586f
     1.1 --- a/src/Pure/term.ML	Tue Mar 11 17:20:59 1997 +0100
     1.2 +++ b/src/Pure/term.ML	Fri Mar 14 10:35:30 1997 +0100
     1.3 @@ -283,6 +283,10 @@
     1.4    | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
     1.5    | loose_bvar _ = false;
     1.6  
     1.7 +fun loose_bvar1(Bound i,k) = i = k
     1.8 +  | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
     1.9 +  | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
    1.10 +  | loose_bvar1 _ = false;
    1.11  
    1.12  (*Substitute arguments for loose bound variables.
    1.13    Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).