1.1 --- a/src/HOL/Tools/metis_tools.ML	Sat Aug 18 13:32:18 2007 +0200
     1.2 +++ b/src/HOL/Tools/metis_tools.ML	Sat Aug 18 13:32:20 2007 +0200
     1.3 @@ -8,8 +8,10 @@
     1.4  signature METIS_TOOLS =
     1.5  sig
     1.6    val type_lits: bool Config.T
     1.7 -  val metis_tac : Proof.context -> thm list -> int -> tactic
     1.8 -  val setup : theory -> theory
     1.9 +  val metis_tac: Proof.context -> thm list -> int -> tactic
    1.10 +  val metisF_tac: Proof.context -> thm list -> int -> tactic
    1.11 +  val metisH_tac: Proof.context -> thm list -> int -> tactic
    1.12 +  val setup: theory -> theory
    1.13  end
    1.14  
    1.15  structure MetisTools: METIS_TOOLS =
    1.16 @@ -91,8 +93,8 @@
    1.17                metis_lit pol "=" (map hol_term_to_fol_HO tms)
    1.18            | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm];
    1.19  
    1.20 -  fun literals_of_hol_thm isFO  t =
    1.21 -        let val (lits, types_sorts) = ResHolClause.literals_of_term t
    1.22 +  fun literals_of_hol_thm thy isFO t =
    1.23 +        let val (lits, types_sorts) = ResHolClause.literals_of_term thy t
    1.24          in  (map (hol_literal_to_fol isFO) lits, types_sorts) end;
    1.25  
    1.26    fun metis_of_typeLit (ResClause.LTVar (s,x))  = metis_lit false s [Metis.Term.Var x]
    1.27 @@ -101,8 +103,9 @@
    1.28    fun metis_of_tfree tf = Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit tf));
    1.29  
    1.30    fun hol_thm_to_fol ctxt isFO th =
    1.31 -    let val (mlits, types_sorts) =
    1.32 -               (literals_of_hol_thm isFO o HOLogic.dest_Trueprop o prop_of) th
    1.33 +    let val thy = ProofContext.theory_of ctxt
    1.34 +        val (mlits, types_sorts) =
    1.35 +               (literals_of_hol_thm thy isFO o HOLogic.dest_Trueprop o prop_of) th
    1.36          val (tvar_lits,tfree_lits) = ResClause.add_typs_aux types_sorts
    1.37          val tlits = if Config.get ctxt type_lits then map metis_of_typeLit tvar_lits else []
    1.38      in  (Metis.Thm.axiom (Metis.LiteralSet.fromList(tlits@mlits)), tfree_lits)  end;
    1.39 @@ -521,8 +524,6 @@
    1.40      let val thy = ProofContext.theory_of ctxt
    1.41          val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause"
    1.42                  else ();
    1.43 -        val _ = ResClause.init thy
    1.44 -        val _ = ResHolClause.init thy
    1.45          val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
    1.46          val _ = app (fn th => Output.debug (fn () => string_of_thm th)) cls
    1.47          val _ = Output.debug (fn () => "THEOREM CLAUSES")