src/HOL/Tools/Nitpick/nitpick_util.ML

 fun pretty_maybe_quote pretty =
   let val s = Pretty.str_of pretty in
     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
 
 end;