src/HOL/Tools/ATP/atp_util.ML

 signature ATP_UTIL =
 sig
   val timestamp : unit -> string
   val hash_string : string -> int
   val hash_term : term -> int
+  val chunk_list : int -> 'a list -> 'a list list
   val stringN_of_int : int -> int -> string
   val strip_spaces : bool -> (char -> bool) -> string -> string
   val strip_spaces_except_between_idents : string -> string
   val elide_string : int -> string -> string
   val nat_subscript : int -> string

   | hashw_term (Free (s, _)) = hashw_string (s, 0w0)
   | hashw_term _ = 0w0
 
 fun hash_string s = Word.toInt (hashw_string (s, 0w0))
 val hash_term = Word.toInt o hashw_term
+
+fun chunk_list _ [] = []
+  | chunk_list k xs =
+    let val (xs1, xs2) = chop k xs in xs1 :: chunk_list k xs2 end
 
 fun stringN_of_int 0 _ = ""
   | stringN_of_int k n =
     stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)