diff -r 8dc52ba4155b -r 4106bc2a9cc8 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Sat Jan 22 12:05:09 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Sat Jan 22 14:00:36 2022 +0100
@@ -49,6 +49,7 @@
   val extract_lambda_def : (term -> string * typ) -> term -> string * term
   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
 end;
 
 structure ATP_Util : ATP_UTIL =
@@ -412,6 +413,11 @@
     else long
   end
 
-  val map_prod = Ctr_Sugar_Util.map_prod
+val map_prod = Ctr_Sugar_Util.map_prod
+
+(* Compare the length of a list with an integer n while traversing at most n elements of the list.
+*)
+fun compare_length_with [] n = if n < 0 then GREATER else if n = 0 then EQUAL else LESS
+  | compare_length_with (_ :: xs) n = if n <= 0 then GREATER else compare_length_with xs (n - 1)
 
 end;