# HG changeset patch
# User wenzelm
# Date 1701959129 -3600
# Node ID 51868d951a4211358ce9c63cce9f701867526f0c
# Parent  04dfecb9343ac6a1683042c52df4f672c126be3d
tuned;

diff -r 04dfecb9343a -r 51868d951a42 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Dec 07 14:48:58 2023 +0100
+++ b/src/Pure/proofterm.ML	Thu Dec 07 15:25:29 2023 +0100
@@ -796,9 +796,9 @@
   let
     val n = length args;
     fun term lev (Bound i) =
-         (if i<lev then raise Same.SAME    (*var is locally bound*)
-          else Term.incr_boundvars lev (nth args (i - lev))
-                  handle General.Subscript => Bound (i - n))  (*loose: change it*)
+         (if i < lev then raise Same.SAME    (*var is locally bound*)
+          else if i - lev < n then Term.incr_boundvars lev (nth args (i - lev))
+          else Bound (i - n))  (*loose: change it*)
       | term lev (Abs (a, T, t)) = Abs (a, T, term (lev + 1) t)
       | term lev (t $ u) = (term lev t $ Same.commit (term lev) u
           handle Same.SAME => t $ term lev u)
@@ -820,8 +820,8 @@
     val n = length args;
     fun proof Plev tlev (PBound i) =
          (if i < Plev then raise Same.SAME    (*var is locally bound*)
-          else incr_boundvars Plev tlev (nth args (i - Plev))
-                 handle General.Subscript => PBound (i - n)  (*loose: change it*))
+          else if i - Plev < n then incr_boundvars Plev tlev (nth args (i - Plev))
+          else PBound (i - n)  (*loose: change it*))
       | proof Plev tlev (AbsP (a, t, p)) = AbsP (a, t, proof (Plev + 1) tlev p)
       | proof Plev tlev (Abst (a, T, p)) = Abst (a, T, proof Plev (tlev + 1) p)
       | proof Plev tlev (p %% q) = (proof Plev tlev p %% Same.commit (proof Plev tlev) q
diff -r 04dfecb9343a -r 51868d951a42 src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Dec 07 14:48:58 2023 +0100
+++ b/src/Pure/term.ML	Thu Dec 07 15:25:29 2023 +0100
@@ -709,8 +709,8 @@
     val n = length args;
     fun term lev (Bound i) =
          (if i < lev then raise Same.SAME   (*var is locally bound*)
-          else incr_boundvars lev (nth args (i - lev))
-            handle General.Subscript => Bound (i - n))  (*loose: change it*)
+          else if i - lev < n then incr_boundvars lev (nth args (i - lev))
+          else Bound (i - n))  (*loose: change it*)
       | term lev (Abs (a, T, t)) = Abs (a, T, term (lev + 1) t)
       | term lev (t $ u) =
           (term lev t $ Same.commit (term lev) u