tuned subst_bound(s);
authorwenzelm
Thu Feb 16 00:09:46 2006 +0100 (2006-02-16)
changeset 1906582e2d66f995b
parent 19064 bf19cc5a7899
child 19066 df24f2564aaa
tuned subst_bound(s);
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Wed Feb 15 23:57:06 2006 +0100
     1.2 +++ b/src/Pure/term.ML	Thu Feb 16 00:09:46 2006 +0100
     1.3 @@ -780,26 +780,32 @@
     1.4       compensate for the disappearance of lambdas.
     1.5  *)
     1.6  fun subst_bounds (args: term list, t) : term =
     1.7 -  let val n = length args;
     1.8 -      fun subst (t as Bound i, lev) =
     1.9 -           (if i<lev then  t    (*var is locally bound*)
    1.10 -            else  incr_boundvars lev (List.nth(args, i-lev))
    1.11 -                    handle Subscript => Bound(i-n)  (*loose: change it*))
    1.12 -        | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
    1.13 -        | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
    1.14 -        | subst (t,lev) = t
    1.15 -  in   case args of [] => t  | _ => subst (t,0)  end;
    1.16 +  let
    1.17 +    exception SAME;
    1.18 +    val n = length args;
    1.19 +    fun subst (t as Bound i, lev) =
    1.20 +         (if i < lev then raise SAME   (*var is locally bound*)
    1.21 +          else incr_boundvars lev (List.nth (args, i - lev))
    1.22 +            handle Subscript => Bound (i - n))  (*loose: change it*)
    1.23 +      | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
    1.24 +      | subst (f $ t, lev) =
    1.25 +          (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
    1.26 +      | subst _ = raise SAME;
    1.27 +  in case args of [] => t | _ => (subst (t, 0) handle SAME => t) end;
    1.28  
    1.29  (*Special case: one argument*)
    1.30  fun subst_bound (arg, t) : term =
    1.31 -  let fun subst (t as Bound i, lev) =
    1.32 -            if i<lev then  t    (*var is locally bound*)
    1.33 -            else  if i=lev then incr_boundvars lev arg
    1.34 -                           else Bound(i-1)  (*loose: change it*)
    1.35 -        | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
    1.36 -        | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
    1.37 -        | subst (t,lev) = t
    1.38 -  in  subst (t,0)  end;
    1.39 +  let
    1.40 +    exception SAME;
    1.41 +    fun subst (Bound i, lev) =
    1.42 +          if i < lev then raise SAME   (*var is locally bound*)
    1.43 +          else if i = lev then incr_boundvars lev arg
    1.44 +          else Bound (i - 1)   (*loose: change it*)
    1.45 +      | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
    1.46 +      | subst (f $ t, lev) =
    1.47 +          (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
    1.48 +      | subst _ = raise SAME;
    1.49 +  in subst (t, 0) handle SAME => t end;
    1.50  
    1.51  (*beta-reduce if possible, else form application*)
    1.52  fun betapply (Abs(_,_,t), u) = subst_bound (u,t)