# HG changeset patch
# User wenzelm
# Date 1701892328 -3600
# Node ID 3b272da1d1651a85a8090958016379193f3a79d8
# Parent  53288743c2f00329d5f7ccc3ea633865a0848b6a
minor performance tuning;

diff -r 53288743c2f0 -r 3b272da1d165 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Wed Dec 06 20:16:23 2023 +0100
+++ b/src/Pure/zterm.ML	Wed Dec 06 20:52:08 2023 +0100
@@ -403,13 +403,15 @@
 fun implies_intr_proof thy A prf =
   let
     val h = global_zterm_of thy A;
-    fun abs_hyp i (p as ZHyp t) = if aconv_zterm (h, t) then ZBoundP i else p
+    fun abs_hyp i (ZHyp t) = if aconv_zterm (h, t) then ZBoundP i else raise Same.SAME
       | abs_hyp i (ZAbst (x, T, p)) = ZAbst (x, T, abs_hyp i p)
       | abs_hyp i (ZAbsP (x, t, p)) = ZAbsP (x, t, abs_hyp (i + 1) p)
       | abs_hyp i (ZAppt (p, t)) = ZAppt (abs_hyp i p, t)
-      | abs_hyp i (ZAppP (p, q)) = ZAppP (abs_hyp i p, abs_hyp i q)
-      | abs_hyp _ p = p;
-  in ZAbsP ("H", h, abs_hyp 0 prf) end;
+      | abs_hyp i (ZAppP (p, q)) =
+          (ZAppP (abs_hyp i p, Same.commit (abs_hyp i) q) handle Same.SAME =>
+            ZAppP (p, abs_hyp i q))
+      | abs_hyp _ _ = raise Same.SAME;
+  in ZAbsP ("H", h, Same.commit (abs_hyp 0) prf) end;
 
 fun forall_intr_proof thy T (a, x) prf =
   let
@@ -421,16 +423,24 @@
       else
         (case b of
           ZAbs (x, T, t) => ZAbs (x, T, abs_term (i + 1) t)
-        | ZApp (t, u) => ZApp (abs_term i t, abs_term i u)
-        | _ => b);
+        | ZApp (t, u) =>
+            (ZApp (abs_term i t, Same.commit (abs_term i) u) handle Same.SAME =>
+              ZApp (t, abs_term i u))
+        | _ => raise Same.SAME);
 
     fun abs_proof i (ZAbst (x, T, prf)) = ZAbst (x, T, abs_proof (i + 1) prf)
-      | abs_proof i (ZAbsP (x, t, prf)) = ZAbsP (x, abs_term i t, abs_proof i prf)
-      | abs_proof i (ZAppt (p, t)) = ZAppt (abs_proof i p, abs_term i t)
-      | abs_proof i (ZAppP (p, q)) = ZAppP (abs_proof i p, abs_proof i q)
-      | abs_proof _ p = p;
+      | abs_proof i (ZAbsP (x, t, prf)) =
+          (ZAbsP (x, abs_term i t, Same.commit (abs_proof i) prf) handle Same.SAME =>
+            ZAbsP (x, t, abs_proof i prf))
+      | abs_proof i (ZAppt (p, t)) =
+          (ZAppt (abs_proof i p, Same.commit (abs_term i) t) handle Same.SAME =>
+            ZAppt (p, abs_term i t))
+      | abs_proof i (ZAppP (p, q)) =
+          (ZAppP (abs_proof i p, Same.commit (abs_proof i) q) handle Same.SAME =>
+            ZAppP (p, abs_proof i q))
+      | abs_proof _ _ = raise Same.SAME;
 
-  in ZAbst (a, Z, abs_proof 0 prf) end;
+  in ZAbst (a, Z, Same.commit (abs_proof 0) prf) end;
 
 fun forall_elim_proof thy t p = ZAppt (p, global_zterm_of thy t);