# HG changeset patch
# User wenzelm
# Date 1702894755 -3600
# Node ID 7c415c73ebf76b4273b462212e1344a93f6dffd6
# Parent  18287f3f48ca10e277b7c02cf390f109eb116015
tuned, following close_proof;

diff -r 18287f3f48ca -r 7c415c73ebf7 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Mon Dec 18 11:15:22 2023 +0100
+++ b/src/Pure/zterm.ML	Mon Dec 18 11:19:15 2023 +0100
@@ -725,13 +725,13 @@
 fun implies_intr_proof thy A prf =
   let
     val h = zterm_of thy A;
-    fun proof i (ZHyp t) = if aconv_zterm (h, t) then ZBoundp i else raise Same.SAME
-      | proof i (ZAbst (x, T, p)) = ZAbst (x, T, proof i p)
-      | proof i (ZAbsp (x, t, p)) = ZAbsp (x, t, proof (i + 1) p)
-      | proof i (ZAppt (p, t)) = ZAppt (proof i p, t)
-      | proof i (ZAppp (p, q)) =
-          (ZAppp (proof i p, Same.commit (proof i) q) handle Same.SAME =>
-            ZAppp (p, proof i q))
+    fun proof lev (ZHyp t) = if aconv_zterm (h, t) then ZBoundp lev else raise Same.SAME
+      | proof lev (ZAbst (x, T, p)) = ZAbst (x, T, proof lev p)
+      | proof lev (ZAbsp (x, t, p)) = ZAbsp (x, t, proof (lev + 1) p)
+      | proof lev (ZAppt (p, t)) = ZAppt (proof lev p, t)
+      | proof lev (ZAppp (p, q)) =
+          (ZAppp (proof lev p, Same.commit (proof lev) q) handle Same.SAME =>
+            ZAppp (p, proof lev q))
       | proof _ _ = raise Same.SAME;
   in ZAbsp ("H", h, Same.commit (proof 0) prf) end;