# HG changeset patch
# User desharna
# Date 1682588818 -7200
# Node ID 55b81d14a1b884f6cc15e357f923e0df222244ab
# Parent  a1abcf46eb24ddad2e35a9feee7839fa7bb4f971
tuned; avoided intermediate list and list traversal

diff -r a1abcf46eb24 -r 55b81d14a1b8 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Apr 27 11:46:11 2023 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Apr 27 11:46:58 2023 +0200
@@ -440,8 +440,7 @@
     q1 = q2 andalso length xs1 = length xs2 andalso
     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)
+    c1 = c2 andalso forall2 (is_same_formula comm subst) phis1 phis2
   | is_same_formula comm subst (AAtom (tm1 as ATerm (("equal", tys), [tm11, tm12]))) (AAtom tm2) =
     is_same_term subst tm1 tm2 orelse
     (comm andalso is_same_term subst (ATerm (("equal", tys), [tm12, tm11])) tm2)
diff -r a1abcf46eb24 -r 55b81d14a1b8 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Thu Apr 27 11:46:11 2023 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Apr 27 11:46:58 2023 +0200
@@ -50,11 +50,16 @@
   val short_thm_name : Proof.context -> thm -> string
   val map_prod : ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> 'b * 'd
   val compare_length_with : 'a list -> int -> order
+  val forall2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
 end;
 
 structure ATP_Util : ATP_UTIL =
 struct
 
+fun forall2 _ [] [] = true
+  | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
+  | forall2 _ _ _ = false
+
 fun timestamp_format time =
   Date.fmt "%Y-%m-%d %H:%M:%S." (Date.fromTimeLocal time) ^
   (StringCvt.padLeft #"0" 3 (string_of_int (Time.toMilliseconds time - 1000 * Time.toSeconds time)))