--- a/src/HOL/Tools/res_atp_methods.ML Fri Nov 18 07:05:11 2005 +0100
+++ b/src/HOL/Tools/res_atp_methods.ML Fri Nov 18 07:06:07 2005 +0100
@@ -25,22 +25,22 @@
(* convert the negated 1st subgoal into CNF, write to files and call an ATP oracle *)
-fun res_atp_tac res_atp_oracle tptp_form make_nnf timeLimit ctxt files tfrees n thm =
+fun res_atp_tac res_atp_oracle tptp_form timeLimit ctxt (helper,files) tfrees n thm =
SELECT_GOAL
((EVERY1 [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac,
METAHYPS(fn negs =>
HEADGOAL(Tactic.rtac
(res_atp_oracle (ProofContext.theory_of ctxt)
- ((tptp_form (make_clauses (map make_nnf negs)) n tfrees)::files, timeLimit))))]) handle Fail _ => no_tac) n thm;
+ ((helper,(tptp_form (make_clauses negs) n tfrees)::files), timeLimit))))]) handle Fail _ => no_tac) n thm;
(* vampire and eprover tactics *)
-val vampireF_tac = res_atp_tac vampire_oracle ResAtpSetup.tptp_form make_nnf (!vampire_time);
+val vampireF_tac = res_atp_tac vampire_oracle ResAtpSetup.tptp_form (!vampire_time);
-val vampireH_tac = res_atp_tac vampire_oracle ResAtpSetup.tptp_formH make_nnf1 (!vampire_time);
+val vampireH_tac = res_atp_tac vampire_oracle ResAtpSetup.tptp_formH (!vampire_time);
-val eproverF_tac = res_atp_tac eprover_oracle ResAtpSetup.tptp_form make_nnf (!eprover_time);
+val eproverF_tac = res_atp_tac eprover_oracle ResAtpSetup.tptp_form (!eprover_time);
-val eproverH_tac = res_atp_tac eprover_oracle ResAtpSetup.tptp_formH make_nnf1 (!eprover_time);
+val eproverH_tac = res_atp_tac eprover_oracle ResAtpSetup.tptp_formH (!eprover_time);
val ResAtps_setup = [Method.add_methods
[("vampireF", ResAtpSetup.atp_method_F vampireF_tac, "A Vampire method for FOL problems"),