Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Thu, 07 Dec 2023 15:25:29 +0100
changeset 79176 51868d951a42
parent 79175 04dfecb9343a
child 79177 b83953ac9494
tuned;
src/Pure/proofterm.ML file | annotate | diff | comparison | revisions
src/Pure/term.ML file | annotate | diff | comparison | revisions 
--- 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
--- 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
isabelle