src/HOL/Tools/res_clause.ML
changeset 18449 e314fb38307d
parent 18439 4b517881ac7e
child 18676 5bce9fddce2e
     1.1 --- a/src/HOL/Tools/res_clause.ML	Wed Dec 21 12:05:47 2005 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Dec 21 12:06:08 2005 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4  
     1.5    (*for hashing*)
     1.6    val clause_eq : clause * clause -> bool
     1.7 -  val hash1_clause : clause -> word
     1.8 +  val hash_clause : clause -> int
     1.9  
    1.10    val list_ord : ('a * 'b -> order) -> 'a list * 'b list -> order
    1.11    type fol_type
    1.12 @@ -659,17 +659,17 @@
    1.13  
    1.14  val xor_words = List.foldl Word.xorb 0w0;
    1.15  
    1.16 -fun hash_term (UVar(_,_), w) = w
    1.17 -  | hash_term (Fun(f,tps,args), w) = 
    1.18 -      List.foldl hash_term (Hashtable.hash_string (f,w)) args;
    1.19 +fun hashw_term (UVar(_,_), w) = w
    1.20 +  | hashw_term (Fun(f,tps,args), w) = 
    1.21 +      List.foldl hashw_term (Polyhash.hashw_string (f,w)) args;
    1.22    
    1.23 -fun hash_pred (Predicate(pn,_,args), w) = 
    1.24 -    List.foldl hash_term (Hashtable.hash_string (pn,w)) args;
    1.25 +fun hashw_pred (Predicate(pn,_,args), w) = 
    1.26 +    List.foldl hashw_term (Polyhash.hashw_string (pn,w)) args;
    1.27      
    1.28 -fun hash1_literal (Literal(true,pred,_)) = hash_pred (pred, 0w0)
    1.29 -  | hash1_literal (Literal(false,pred,_)) = Word.notb (hash_pred (pred, 0w0));
    1.30 +fun hash1_literal (Literal(true,pred,_)) = hashw_pred (pred, 0w0)
    1.31 +  | hash1_literal (Literal(false,pred,_)) = Word.notb (hashw_pred (pred, 0w0));
    1.32    
    1.33 -fun hash1_clause clause = xor_words (map hash1_literal (get_literals clause));
    1.34 +fun hash_clause clause = Word.toIntX (xor_words (map hash1_literal (get_literals clause)));
    1.35  
    1.36  
    1.37  (* FIX: not sure what to do with these funcs *)