# HG changeset patch
# User wenzelm
# Date 1702209271 -3600
# Node ID f3e7822deb1cb524a555780809e806211be7d6de
# Parent  b79030f610cad0b83ee95ab18aa1b41c3997c46f
tuned;

diff -r b79030f610ca -r f3e7822deb1c src/Pure/logic.ML
--- 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;