diff -r 2477286fcc7e -r 944705cc79d2 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Sat Aug 18 13:32:18 2007 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Sat Aug 18 13:32:20 2007 +0200
@@ -8,8 +8,10 @@
 signature METIS_TOOLS =
 sig
   val type_lits: bool Config.T
-  val metis_tac : Proof.context -> thm list -> int -> tactic
-  val setup : theory -> theory
+  val metis_tac: Proof.context -> thm list -> int -> tactic
+  val metisF_tac: Proof.context -> thm list -> int -> tactic
+  val metisH_tac: Proof.context -> thm list -> int -> tactic
+  val setup: theory -> theory
 end
 
 structure MetisTools: METIS_TOOLS =
@@ -91,8 +93,8 @@
               metis_lit pol "=" (map hol_term_to_fol_HO tms)
           | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm];
 
-  fun literals_of_hol_thm isFO  t =
-        let val (lits, types_sorts) = ResHolClause.literals_of_term t
+  fun literals_of_hol_thm thy isFO t =
+        let val (lits, types_sorts) = ResHolClause.literals_of_term thy t
         in  (map (hol_literal_to_fol isFO) lits, types_sorts) end;
 
   fun metis_of_typeLit (ResClause.LTVar (s,x))  = metis_lit false s [Metis.Term.Var x]
@@ -101,8 +103,9 @@
   fun metis_of_tfree tf = Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit tf));
 
   fun hol_thm_to_fol ctxt isFO th =
-    let val (mlits, types_sorts) =
-               (literals_of_hol_thm isFO o HOLogic.dest_Trueprop o prop_of) th
+    let val thy = ProofContext.theory_of ctxt
+        val (mlits, types_sorts) =
+               (literals_of_hol_thm thy isFO o HOLogic.dest_Trueprop o prop_of) th
         val (tvar_lits,tfree_lits) = ResClause.add_typs_aux types_sorts
         val tlits = if Config.get ctxt type_lits then map metis_of_typeLit tvar_lits else []
     in  (Metis.Thm.axiom (Metis.LiteralSet.fromList(tlits@mlits)), tfree_lits)  end;
@@ -521,8 +524,6 @@
     let val thy = ProofContext.theory_of ctxt
         val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause"
                 else ();
-        val _ = ResClause.init thy
-        val _ = ResHolClause.init thy
         val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
         val _ = app (fn th => Output.debug (fn () => string_of_thm th)) cls
         val _ = Output.debug (fn () => "THEOREM CLAUSES")