# HG changeset patch
# User wenzelm
# Date 1140044986 -3600
# Node ID 82e2d66f995bcd77a216bcef08beb6428086f542
# Parent  bf19cc5a789991ff599ac8ba82f586bb2ce21f4e
tuned subst_bound(s);

diff -r bf19cc5a7899 -r 82e2d66f995b src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Feb 15 23:57:06 2006 +0100
+++ b/src/Pure/term.ML	Thu Feb 16 00:09:46 2006 +0100
@@ -780,26 +780,32 @@
      compensate for the disappearance of lambdas.
 *)
 fun subst_bounds (args: term list, t) : term =
-  let val n = length args;
-      fun subst (t as Bound i, lev) =
-           (if i<lev then  t    (*var is locally bound*)
-            else  incr_boundvars lev (List.nth(args, i-lev))
-                    handle Subscript => Bound(i-n)  (*loose: change it*))
-        | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
-        | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
-        | subst (t,lev) = t
-  in   case args of [] => t  | _ => subst (t,0)  end;
+  let
+    exception SAME;
+    val n = length args;
+    fun subst (t as Bound i, lev) =
+         (if i < lev then raise SAME   (*var is locally bound*)
+          else incr_boundvars lev (List.nth (args, i - lev))
+            handle Subscript => Bound (i - n))  (*loose: change it*)
+      | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
+      | subst (f $ t, lev) =
+          (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
+      | subst _ = raise SAME;
+  in case args of [] => t | _ => (subst (t, 0) handle SAME => t) end;
 
 (*Special case: one argument*)
 fun subst_bound (arg, t) : term =
-  let fun subst (t as Bound i, lev) =
-            if i<lev then  t    (*var is locally bound*)
-            else  if i=lev then incr_boundvars lev arg
-                           else Bound(i-1)  (*loose: change it*)
-        | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
-        | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
-        | subst (t,lev) = t
-  in  subst (t,0)  end;
+  let
+    exception SAME;
+    fun subst (Bound i, lev) =
+          if i < lev then raise SAME   (*var is locally bound*)
+          else if i = lev then incr_boundvars lev arg
+          else Bound (i - 1)   (*loose: change it*)
+      | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
+      | subst (f $ t, lev) =
+          (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
+      | subst _ = raise SAME;
+  in subst (t, 0) handle SAME => t end;
 
 (*beta-reduce if possible, else form application*)
 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)