# HG changeset patch
# User paulson
# Date 1158853197 -7200
# Node ID 9116dc6842e103e30d992edfe118899f258c5d54
# Parent  46832fee12157cd273d482be2ba0bef7a70406ae
new function hashw_int

diff -r 46832fee1215 -r 9116dc6842e1 src/HOL/Tools/polyhash.ML
--- 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;