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