tuned;

--- a/src/Pure/logic.ML	Sun Dec 10 12:18:22 2023 +0100
+++ b/src/Pure/logic.ML	Sun Dec 10 12:54:31 2023 +0100
@@ -467,10 +467,10 @@
                 combound (Free (x, Ts ---> Same.commit incrT T), lev, n)
               else Free (x, incrT T)
           | incr lev (Abs (x, T, body)) =
-              (Abs (x, incrT T, incr (lev + 1) body handle Same.SAME => body)
+              (Abs (x, incrT T, Same.commit (incr (lev + 1)) body)
                 handle Same.SAME => Abs (x, T, incr (lev + 1) body))
           | incr lev (t $ u) =
-              (incr lev t $ (incr lev u handle Same.SAME => u)
+              (incr lev t $ Same.commit (incr lev) u
                 handle Same.SAME => t $ incr lev u)
           | incr _ (Const (c, T)) = Const (c, incrT T)
           | incr _ (Bound _) = raise Same.SAME;