--- 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)
--- 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)))