src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 36062 194cb6e3c13f
parent 35994 9cc3df9a606e
child 36126 00d550b6cfd4
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 29 15:26:19 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 29 15:50:18 2010 +0200
     1.3 @@ -217,6 +217,7 @@
     1.4  structure Nitpick_HOL : NITPICK_HOL =
     1.5  struct
     1.6  
     1.7 +open Sledgehammer_Util
     1.8  open Nitpick_Util
     1.9  
    1.10  type const_table = term list Symtab.table
    1.11 @@ -1229,8 +1230,8 @@
    1.12    | is_ground_term _ = false
    1.13  
    1.14  (* term -> word -> word *)
    1.15 -fun hashw_term (t1 $ t2) = Polyhash.hashw (hashw_term t1, hashw_term t2)
    1.16 -  | hashw_term (Const (s, _)) = Polyhash.hashw_string (s, 0w0)
    1.17 +fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
    1.18 +  | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
    1.19    | hashw_term _ = 0w0
    1.20  (* term -> int *)
    1.21  val hash_term = Word.toInt o hashw_term