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