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