# HG changeset patch
# User blanchet
# Date 1378821411 -7200
# Node ID 412f8c590c6cd55b291a0712e768ec43a92aee30
# Parent  9750618c32edf007871ce67fb872830fda9c81b9
moved ML function closer to its remaining use

diff -r 9750618c32ed -r 412f8c590c6c src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Tue Sep 10 15:56:51 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Sep 10 15:56:51 2013 +0200
@@ -8,7 +8,6 @@
 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
@@ -63,13 +62,7 @@
 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 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)
-  | 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 =
diff -r 9750618c32ed -r 412f8c590c6c src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Sep 10 15:56:51 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Sep 10 15:56:51 2013 +0200
@@ -299,6 +299,11 @@
     if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty]
   end
 
-val hash_term = ATP_Util.hash_term
+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)
+  | hashw_term _ = 0w0
+
+val hash_term = Word.toInt o hashw_term
 
 end;