# HG changeset patch
# User wenzelm
# Date 1702931499 -3600
# Node ID 5a5d0c36ade8378aeb66a0d29d31f5cf9007f208
# Parent  28342f38da5c365c1e9a6cbec921bc542806c4e2
tuned;

diff -r 28342f38da5c -r 5a5d0c36ade8 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Dec 18 14:42:41 2023 +0100
+++ b/src/Pure/proofterm.ML	Mon Dec 18 21:31:39 2023 +0100
@@ -811,9 +811,9 @@
   let
     val n = length args;
     fun proof Plev tlev (PBound i) =
-         (if i < Plev then raise Same.SAME    (*var is locally bound*)
+          if i < Plev then raise Same.SAME    (*var is locally bound*)
           else if i - Plev < n then incr_boundvars Plev tlev (nth args (i - Plev))
-          else PBound (i - n)  (*loose: change it*))
+          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) =
diff -r 28342f38da5c -r 5a5d0c36ade8 src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Dec 18 14:42:41 2023 +0100
+++ b/src/Pure/term.ML	Mon Dec 18 21:31:39 2023 +0100
@@ -711,9 +711,9 @@
     let
       val n = length args;
       fun term lev (Bound i) =
-           (if i < lev then raise Same.SAME   (*var is locally bound*)
+            if i < lev then raise Same.SAME   (*var is locally bound*)
             else if i - lev < n then incr_boundvars lev (nth args (i - lev))
-            else Bound (i - n))  (*loose: change it*)
+            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