src/HOL/Tools/res_axioms.ML

        |> transform_elim |> zero_var_indexes |> freeze_thm
        |> ObjectLogic.atomize_thm |> make_nnf |> strip_lambdas ~1;
 
 (*The cache prevents repeated clausification of a theorem,
   and also repeated declaration of Skolem functions*)
-  (* FIXME better use Termtab!? No, we MUST use theory data!!*)
-val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table)
+  (* FIXME  use theory data!!*)
+val clause_cache = ref (Thmtab.empty : thm list Thmtab.table)
 
 
 (*Generate Skolem functions for a theorem supplied in nnf*)
 fun skolem_of_nnf th =
   map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th);

 (*Keep the full complexity of the original name*)
 fun flatten_name s = space_implode "_X" (NameSpace.explode s);
 
 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
   It returns a modified theory, unless skolemization fails.*)
-fun skolem thy (name,th) =
-  let val cname = (case name of "" => gensym "" | s => flatten_name s)
-      val _ = Output.debug (fn () => "skolemizing " ^ name ^ ": ")
+fun skolem thy th =
+  let val cname = (case PureThy.get_name_hint th of "" => gensym "" | s => flatten_name s)
+      val _ = Output.debug (fn () => "skolemizing " ^ cname ^ ": ")
   in Option.map
         (fn nnfth =>
           let val (thy',defs) = declare_skofuns cname nnfth thy
               val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
               val (thy'',cnfs') = declare_abstract (thy',cnfs)

       (SOME (to_nnf th)  handle THM _ => NONE)
   end;
 
 (*Populate the clause cache using the supplied theorem. Return the clausal form
   and modified theory.*)
-fun skolem_cache_thm (name,th) thy =
-  case Symtab.lookup (!clause_cache) name of
+fun skolem_cache_thm th thy =
+  case Thmtab.lookup (!clause_cache) th of
       NONE =>
-        (case skolem thy (name, Thm.transfer thy th) of
+        (case skolem thy (Thm.transfer thy th) of
              NONE => ([th],thy)
            | SOME (cls,thy') => 
-                 (if null cls then warning ("skolem_cache: empty clause set for " ^ name)
+                 (if null cls 
+                  then warning ("skolem_cache: empty clause set for " ^ string_of_thm th)
                   else ();
-                  change clause_cache (Symtab.update (name, (th, cls))); 
+                  change clause_cache (Thmtab.update (th, cls)); 
                   (cls,thy')))
-    | SOME (th',cls) =>
-        if Thm.eq_thm(th,th') then (cls,thy)
-        else (Output.debug (fn () => "skolem_cache: Ignoring variant of theorem " ^ name);
-              Output.debug (fn () => string_of_thm th);
-              Output.debug (fn () => string_of_thm th');
-              getOpt (skolem thy (name, Thm.transfer thy th), ([th],thy)));
+    | SOME cls => (cls,thy);
 
 (*Exported function to convert Isabelle theorems into axiom clauses*)
-fun cnf_axiom (name,th) =
- (Output.debug (fn () => "cnf_axiom called, theorem name = " ^ name);
-  case name of
-        "" => skolem_thm th (*no name, so can't cache*)
-      | s  => case Symtab.lookup (!clause_cache) s of
-                NONE => 
-                  let val cls = map Goal.close_result (skolem_thm th)
-                  in Output.debug (fn () => "inserted into cache");
-                     change clause_cache (Symtab.update (s, (th, cls))); cls 
-                  end
-              | SOME(th',cls) =>
-                  if Thm.eq_thm(th,th') then cls
-                  else
-                    (Output.debug (fn () => "cnf_axiom: duplicate or variant of theorem " ^ name);
-                     Output.debug (fn () => string_of_thm th);
-                     Output.debug (fn () => string_of_thm th');
-                     skolem_thm th)
- );
+fun cnf_axiom th =
+  case Thmtab.lookup (!clause_cache) th of
+      NONE => 
+	let val cls = map Goal.close_result (skolem_thm th)
+	in Output.debug (fn () => "inserted into cache");
+	   change clause_cache (Thmtab.update (th, cls)); cls 
+	end
+    | SOME cls => cls;
 
 fun pairname th = (PureThy.get_name_hint th, th);
-
-(*Principally for debugging*)
-fun cnf_name s = 
-  let val th = thm s
-  in cnf_axiom (PureThy.get_name_hint th, th) end;
 
 (**** Extract and Clausify theorems from a theory's claset and simpset ****)
 
 fun rules_of_claset cs =
   let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs

 fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt);
 
 fun atpset_rules_of ctxt = map pairname (ResAtpset.get_atpset ctxt);
 
 
-(**** Translate a set of classical/simplifier rules into CNF (still as type "thm")  ****)
+(**** Translate a set of theorems into CNF ****)
 
 (* classical rules: works for both FOL and HOL *)
 fun cnf_rules [] err_list = ([],err_list)
   | cnf_rules ((name,th) :: ths) err_list =
       let val (ts,es) = cnf_rules ths err_list
-      in  (cnf_axiom (name,th) :: ts,es) handle  _ => (ts, (th::es))  end;
+      in  (cnf_axiom th :: ts,es) handle  _ => (ts, (th::es))  end;
 
 fun pair_name_cls k (n, []) = []
   | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
 
 fun cnf_rules_pairs_aux pairs [] = pairs
   | cnf_rules_pairs_aux pairs ((name,th)::ths) =
-      let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) @ pairs
+      let val pairs' = (pair_name_cls 0 (name, cnf_axiom th)) @ pairs
                        handle THM _ => pairs | ResClause.CLAUSE _ => pairs
       in  cnf_rules_pairs_aux pairs' ths  end;
 
 (*The combination of rev and tail recursion preserves the original order*)
 fun cnf_rules_pairs l = cnf_rules_pairs_aux [] (rev l);

 
 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
 
 (*Setup function: takes a theory and installs ALL known theorems into the clause cache*)
 
-fun skolem_cache (name,th) thy =
+fun skolem_cache th thy =
   let val prop = Thm.prop_of th
   in
       if lambda_free prop 
          (*Monomorphic theorems can be Skolemized on demand,
            but there are problems with re-use of abstraction functions if we don't
            do them now, even for monomorphic theorems.*)
       then thy  
-      else #2 (skolem_cache_thm (name,th) thy)
+      else #2 (skolem_cache_thm th thy)
   end;
 
 (*The cache can be kept smaller by augmenting the condition above with 
     orelse (not abstract_lambdas andalso monomorphic prop).
   However, while this step does not reduce the time needed to build HOL, 
   it doubles the time taken by the first call to the ATP link-up.*)
 
-fun clause_cache_setup thy = fold skolem_cache (PureThy.all_thms_of thy) thy;
+fun clause_cache_setup thy = fold skolem_cache (map #2 (PureThy.all_thms_of thy)) thy;
 
 
 (*** meson proof methods ***)
 
 fun skolem_use_cache_thm th =
-  case Symtab.lookup (!clause_cache) (PureThy.get_name_hint th) of
+  case Thmtab.lookup (!clause_cache) th of
       NONE => skolem_thm th
-    | SOME (th',cls) =>
-        if Thm.eq_thm(th,th') then cls else skolem_thm th;
+    | SOME cls => cls;
 
 fun cnf_rules_of_ths ths = List.concat (map skolem_use_cache_thm ths);
 
 val meson_method_setup = Method.add_methods
   [("meson", Method.thms_args (fn ths =>
       Method.SIMPLE_METHOD' (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs)),
     "MESON resolution proof procedure")];
 
 (** Attribute for converting a theorem into clauses **)
 
-fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom (pairname th));
+fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom th);
 
 fun clausify_rule (th,i) = List.nth (meta_cnf_axiom th, i)
 
 val clausify = Attrib.syntax (Scan.lift Args.nat
   >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
 
 
 (*** Converting a subgoal into negated conjecture clauses. ***)
 
 val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac];
-val neg_clausify = Meson.finish_cnf o assume_abstract_list o make_clauses;
+
+(*finish_cnf removes tautologies and functional reflexivity axioms, but by calling Thm.varifyT
+  it can introduce TVars, which we don't want in conjecture clauses.*)
+val neg_clausify = map Thm.freezeT o Meson.finish_cnf o assume_abstract_list o make_clauses;
 
 fun neg_conjecture_clauses st0 n =
   let val st = Seq.hd (neg_skolemize_tac n st0)
       val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st))
   in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end;

 (*Conjoin a list of theorems to form a single theorem*)
 fun conj_rule []  = TrueI
   | conj_rule ths = foldr1 conj2_rule ths;
 
 fun skolem_attr (Context.Theory thy, th) =
-      let val name = PureThy.get_name_hint th
-          val (cls, thy') = skolem_cache_thm (name, th) thy
+      let val (cls, thy') = skolem_cache_thm th thy
       in (Context.Theory thy', conj_rule cls) end
   | skolem_attr (context, th) = (context, conj_rule (skolem_use_cache_thm th));
 
 val setup_attrs = Attrib.add_attributes
   [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"),