# HG changeset patch
# User blanchet
# Date 1378821722 -7200
# Node ID fa5b34ffe4a400a674ac5d89b98cb3b9b1fdc7da
# Parent  1082a6fb36c6d412c7bc46947c4323d0ae10d44a
sorted out dependencies

diff -r 1082a6fb36c6 -r fa5b34ffe4a4 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Tue Sep 10 15:56:52 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Sep 10 16:02:02 2013 +0200
@@ -7,6 +7,8 @@
 signature ATP_UTIL =
 sig
   val timestamp : unit -> string
+  val hashw : word * word -> word
+  val hashw_string : string * word -> word
   val hash_string : string -> int
   val chunk_list : int -> 'a list -> 'a list list
   val stringN_of_int : int -> int -> string
diff -r 1082a6fb36c6 -r fa5b34ffe4a4 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Sep 10 15:56:52 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Sep 10 16:02:02 2013 +0200
@@ -299,9 +299,9 @@
     if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty]
   end
 
-fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
-  | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
-  | hashw_term (Free (s, _)) = hashw_string (s, 0w0)
+fun hashw_term (t1 $ t2) = ATP_Util.hashw (hashw_term t1, hashw_term t2)
+  | hashw_term (Const (s, _)) = ATP_Util.hashw_string (s, 0w0)
+  | hashw_term (Free (s, _)) = ATP_Util.hashw_string (s, 0w0)
   | hashw_term _ = 0w0
 
 val hash_term = Word.toInt o hashw_term