# HG changeset patch
# User paulson
# Date 1158852791 -7200
# Node ID 46832fee12157cd273d482be2ba0bef7a70406ae
# Parent  8606ddd42554810da64c7e714238af36c8dcbde8
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
unless theorems differ by sorts alone, which should not matter. Also minor fixes to
standard hashing.

diff -r 8606ddd42554 -r 46832fee1215 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Sep 21 17:31:10 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu Sep 21 17:33:11 2006 +0200
@@ -456,12 +456,6 @@
 
 (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
 
-fun fake_thm_name th = 
-    Context.theory_name (theory_of_thm th) ^ "." ^ gensym"";
-
-fun put_name_pair ("",th) = (fake_thm_name th, th)
-  | put_name_pair (a,th)  = (a,th);
-
 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
 
 exception HASH_CLAUSE and HASH_STRING;
@@ -501,9 +495,9 @@
 val xor_words = List.foldl Word.xorb 0w0;
 
 fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w)
-  | hashw_term ((Free(_,_)), w) = w
+  | hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
   | hashw_term ((Var(_,_)), w) = w
-  | hashw_term ((Bound _), w) = w
+  | hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
   | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
   | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
 
@@ -524,6 +518,26 @@
 
 fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));
 
+(*Versions ONLY for "faking" a theorem name. Here we take variable names into account
+  so that similar theorems don't collide.  FIXME: this entire business of "faking" 
+  theorem names must end!*)
+fun hashw_typ (TVar ((a,i), _), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w))
+  | hashw_typ (TFree (a,_), w) = Polyhash.hashw_string (a,w)
+  | hashw_typ (Type (a, Ts), w) = Polyhash.hashw_string (a, List.foldl hashw_typ w Ts);
+
+fun full_hashw_term ((Const(c,T)), w) = Polyhash.hashw_string (c, hashw_typ(T,w))
+  | full_hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
+  | full_hashw_term ((Var((a,i),_)), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w))
+  | full_hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
+  | full_hashw_term ((Abs(_,T,t)), w) = full_hashw_term (t, hashw_typ(T,w))
+  | full_hashw_term ((P$Q), w) = full_hashw_term (Q, (full_hashw_term (P, w)));
+
+fun full_hashw_thm (th,w) = 
+  let val {prop,hyps,...} = rep_thm th
+  in List.foldl full_hashw_term w (prop::hyps) end
+
+fun full_hash_thm th = full_hashw_thm (th,0w0);
+
 fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
 
 (*Create a hash table for clauses, of the given size*)
@@ -556,6 +570,12 @@
 fun get_relevant_clauses thy cls_thms white_cls goals =
   insert_thms white_cls (ReduceAxiomsN.relevance_filter thy cls_thms goals);
 
+(*This name is cryptic but short. Unlike gensym, we get the same name each time.*)
+fun fake_thm_name th = 
+    Context.theory_name (theory_of_thm th) ^ "." ^ Word.toString (full_hash_thm th);
+
+fun put_name_pair ("",th) = (fake_thm_name th, th)
+  | put_name_pair (a,th)  = (a,th);
 
 fun display_thms [] = ()
   | display_thms ((name,thm)::nthms) =