diff -r 2b094d17f432 -r 62d64709af3b src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Jul 14 15:14:38 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Jul 14 16:50:05 2011 +0200
@@ -79,8 +79,7 @@
   val pstrs : string -> Pretty.T list
   val unyxml : string -> string
   val pretty_maybe_quote : Pretty.T -> Pretty.T
-  val hashw : word * word -> word
-  val hashw_string : string * word -> word
+  val hash_term : term -> int
 end;
 
 structure Nitpick_Util : NITPICK_UTIL =
@@ -298,7 +297,6 @@
     if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty]
   end
 
-val hashw = ATP_Util.hashw
-val hashw_string = ATP_Util.hashw_string
+val hash_term = ATP_Util.hash_term
 
 end;