# HG changeset patch
# User desharna
# Date 1682588771 -7200
# Node ID a1abcf46eb24ddad2e35a9feee7839fa7bb4f971
# Parent  ce09ea4c0f931e60458a70aa614890286fb2471d
tuned; avoided intermediate lists

diff -r ce09ea4c0f93 -r a1abcf46eb24 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Apr 27 11:17:53 2023 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Apr 27 11:46:11 2023 +0200
@@ -438,7 +438,7 @@
 
 fun is_same_formula comm subst (AQuant (q1, xs1, phi1)) (AQuant (q2, xs2, phi2)) =
     q1 = q2 andalso length xs1 = length xs2 andalso
-    is_same_formula comm ((map fst xs1 ~~ map fst xs2) @ subst) phi1 phi2
+    is_same_formula comm (map2 (fn (x1, _) => fn (x2, _) => (x1, x2)) xs1 xs2 @ subst) phi1 phi2
   | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) =
     c1 = c2 andalso length phis1 = length phis2 andalso
     forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2)