# HG changeset patch
# User wenzelm
# Date 1702209292 -3600
# Node ID 6ad172f08c4320871f38a5b08d21132379881532
# Parent  f3e7822deb1cb524a555780809e806211be7d6de
tuned;

diff -r f3e7822deb1c -r 6ad172f08c43 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sun Dec 10 12:54:31 2023 +0100
+++ b/src/Pure/logic.ML	Sun Dec 10 12:54:52 2023 +0100
@@ -466,9 +466,9 @@
               if member (op =) fixed x then
                 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, Same.commit (incr (lev + 1)) body)
-                handle Same.SAME => Abs (x, T, incr (lev + 1) body))
+          | incr lev (Abs (x, T, t)) =
+              (Abs (x, incrT T, Same.commit (incr (lev + 1)) t)
+                handle Same.SAME => Abs (x, T, incr (lev + 1) t))
           | incr lev (t $ u) =
               (incr lev t $ Same.commit (incr lev) u
                 handle Same.SAME => t $ incr lev u)