diff -r 8a8d71e34297 -r 7b5f7ca25d17 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -9,6 +9,7 @@
   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
@@ -67,6 +68,10 @@
 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)