Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Sun, 10 Dec 2023 12:54:52 +0100
changeset 79231 6ad172f08c43
parent 79230 f3e7822deb1c
child 79232 99bc2dd45111
tuned;
src/Pure/logic.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle