# HG changeset patch
# User wenzelm
# Date 1702933873 -3600
# Node ID 3c542c1087f102b4bb09ebd1037472c46fbed211
# Parent  ec213a5fda36aa2bdffce0080f700ea52eacd544
tuned whitespace;

diff -r ec213a5fda36 -r 3c542c1087f1 src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Dec 18 21:52:55 2023 +0100
+++ b/src/Pure/term.ML	Mon Dec 18 22:11:13 2023 +0100
@@ -634,11 +634,12 @@
   if inc = 0 then fn _ => Same.same
   else
     let
-      fun term lev (Bound i) = if i >= lev then Bound (i + inc) else raise Same.SAME
+      fun term lev (Bound i) =
+            if i >= lev then Bound (i + inc) else raise Same.SAME
         | 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)
+            (term lev t $ Same.commit (term lev) u
+              handle Same.SAME => t $ term lev u)
         | term _ _ = raise Same.SAME;
     in term end;
 
diff -r ec213a5fda36 -r 3c542c1087f1 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Mon Dec 18 21:52:55 2023 +0100
+++ b/src/Pure/zterm.ML	Mon Dec 18 22:11:13 2023 +0100
@@ -347,11 +347,12 @@
   if inc = 0 then fn _ => Same.same
   else
     let
-      fun term lev (ZBound i) = if i >= lev then ZBound (i + inc) else raise Same.SAME
+      fun term lev (ZBound i) =
+            if i >= lev then ZBound (i + inc) else raise Same.SAME
         | term lev (ZAbs (a, T, t)) = ZAbs (a, T, term (lev + 1) t)
         | term lev (ZApp (t, u)) =
-            (ZApp (term lev t, Same.commit (term lev) u) handle Same.SAME =>
-              ZApp (t, term lev u))
+            (ZApp (term lev t, Same.commit (term lev) u)
+              handle Same.SAME => ZApp (t, term lev u))
         | term _ _ = raise Same.SAME;
     in term end;