--- a/src/HOL/Tools/polyhash.ML Thu Sep 21 17:33:11 2006 +0200
+++ b/src/HOL/Tools/polyhash.ML Thu Sep 21 17:39:57 2006 +0200
@@ -36,6 +36,7 @@
(*Additions due to L. C. Paulson and Jia Meng*)
val hashw : word * word -> word
val hashw_char : Char.char * word -> word
+val hashw_int : int * word -> word
val hashw_vector : word Vector.vector * word -> word
val hashw_string : string * word -> word
val hashw_strings : string list * word -> word
@@ -392,6 +393,8 @@
fun hashw_char (c,w) = hashw (Word.fromInt (Char.ord c), w);
+ fun hashw_int (i,w) = hashw (Word.fromInt i, w);
+
fun hashw_vector (v,w) = Vector.foldl hashw w v;
fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s;