src/HOL/Tools/ATP/atp_problem.ML

--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue May 31 16:38:36 2011 +0200
@@ -70,9 +70,6 @@
     -> 'd -> 'd
   val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
   val is_format_typed : format -> bool
-  val timestamp : unit -> string
-  val hashw : word * word -> word
-  val hashw_string : string * word -> word
   val tptp_strings_for_atp_problem : format -> string problem -> string list
   val filter_cnf_ueq_problem :
     (string * string) problem -> (string * string) problem
@@ -87,6 +84,9 @@
 structure ATP_Problem : ATP_PROBLEM =
 struct
 
+open ATP_Util
+
+
 (** ATP problem **)
 
 datatype 'a fo_term = ATerm of 'a * 'a fo_term list
@@ -172,15 +172,6 @@
 
 val is_format_typed = member (op =) [TFF, THF]
 
-val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
-
-(* This hash function is recommended in "Compilers: Principles, Techniques, and
-   Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they
-   particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
-fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
-fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
-fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s
-
 fun string_for_kind Axiom = "axiom"
   | string_for_kind Definition = "definition"
   | string_for_kind Lemma = "lemma"