--- 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) =
--- 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