new function hashw_int
authorpaulson
Thu Sep 21 17:39:57 2006 +0200 (2006-09-21)
changeset 206629116dc6842e1
parent 20661 46832fee1215
child 20663 2024d9f7df9c
new function hashw_int
src/HOL/Tools/polyhash.ML
     1.1 --- a/src/HOL/Tools/polyhash.ML	Thu Sep 21 17:33:11 2006 +0200
     1.2 +++ b/src/HOL/Tools/polyhash.ML	Thu Sep 21 17:39:57 2006 +0200
     1.3 @@ -36,6 +36,7 @@
     1.4  (*Additions due to L. C. Paulson and Jia Meng*)
     1.5  val hashw : word * word -> word
     1.6  val hashw_char : Char.char * word -> word
     1.7 +val hashw_int : int * word -> word
     1.8  val hashw_vector : word Vector.vector * word -> word
     1.9  val hashw_string : string * word -> word
    1.10  val hashw_strings : string list * word -> word
    1.11 @@ -392,6 +393,8 @@
    1.12  
    1.13     fun hashw_char (c,w) = hashw (Word.fromInt (Char.ord c), w);
    1.14     
    1.15 +   fun hashw_int (i,w) = hashw (Word.fromInt i, w);
    1.16 +   
    1.17     fun hashw_vector (v,w) = Vector.foldl hashw w v;
    1.18     
    1.19     fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s;