# HG changeset patch
# User wenzelm
# Date 1702325364 -3600
# Node ID f1415f78f7a0fec96a7a12fbe33cbad2eb71557e
# Parent  a32428d81fe56c661294c97f2bb315fdf307aa21
minor performance tuning: prefer Same.operation;

diff -r a32428d81fe5 -r f1415f78f7a0 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Dec 11 20:53:01 2023 +0100
+++ b/src/Pure/thm.ML	Mon Dec 11 21:09:24 2023 +0100
@@ -2261,15 +2261,15 @@
     if null vars andalso null bounds then NONE
     else
       let
-        fun rename (t as Var ((x, i), T)) =
-              (case AList.lookup (op =) vars x of
-                 SOME y => Var ((y, i), T)
-               | NONE => t)
-          | rename (Abs (x, T, t)) =
-              Abs (perhaps (AList.lookup (op =) bounds) x, T, rename t)
-          | rename (f $ t) = rename f $ rename t
-          | rename t = t;
-      in SOME rename end
+        fun term (Var ((x, i), T)) =
+              let val y = perhaps (AList.lookup (op =) vars) x
+              in if x = y then raise Same.SAME else Var ((y, i), T) end
+          | term (Abs (x, T, t)) =
+              let val y = perhaps (AList.lookup (op =) bounds) x
+              in if x = y then Abs (x, T, term t) else Abs (y, T, Same.commit term t) end
+          | term (t $ u) = (term t $ Same.commit term u handle Same.SAME => t $ term u)
+          | term _ = raise Same.SAME;
+      in SOME term end
   end;
 
 
@@ -2381,9 +2381,9 @@
             NONE => (As0, rder)
           | SOME f =>
               let
-                fun proof p = Proofterm.map_proof_terms f I p;
+                fun proof p = Same.commit (Proofterm.map_proof_terms_same f I) p;
                 fun zproof p = ZTerm.todo_proof p;
-              in (map (strip_apply f B) As0, deriv_rule1 zproof proof rder) end);
+              in (map (strip_apply (Same.commit f) B) As0, deriv_rule1 zproof proof rder) end);
       in
         (if flatten then map (Logic.flatten_params n) As1 else As1, As1, rder', n)
           handle TERM _ => raise THM("bicompose: 1st premise", 0, [orule])