# HG changeset patch
# User wenzelm
# Date 1187436742 -7200
# Node ID e9d99744e40c61434b1d622481dd1a55f38d1b1e
# Parent  ea5be4be3bae41f06cd0ca69e9f207523868a77c
proper signature;

diff -r ea5be4be3bae -r e9d99744e40c src/HOL/Tools/res_atp_methods.ML
--- a/src/HOL/Tools/res_atp_methods.ML	Sat Aug 18 13:32:21 2007 +0200
+++ b/src/HOL/Tools/res_atp_methods.ML	Sat Aug 18 13:32:22 2007 +0200
@@ -2,18 +2,34 @@
    Author: Jia Meng, NICTA
 *)
 
+signature RES_ATP_METHODS =
+sig
+  val vampire_tac: Proof.context -> thm list -> int -> tactic
+  val eprover_tac: Proof.context -> thm list -> int -> tactic
+  val spass_tac: Proof.context -> thm list -> int -> tactic
+  val vampireF_tac: Proof.context -> thm list -> int -> tactic
+  val vampireH_tac: Proof.context -> thm list -> int -> tactic
+  val eproverF_tac: Proof.context -> thm list -> int -> tactic
+  val eproverH_tac: Proof.context -> thm list -> int -> tactic
+  val spassF_tac: Proof.context -> thm list -> int -> tactic
+  val spassH_tac: Proof.context -> thm list -> int -> tactic
+  val setup: theory -> theory
+end
 
 structure ResAtpMethods =
+struct
 
-struct
-  
 (* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *)
-fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms n thm =
-    (EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac,
-		  METAHYPS(fn negs =>
-			      HEADGOAL(Tactic.rtac 
-					   (res_atp_oracle (ProofContext.theory_of ctxt) 
-							   (ResAtp.write_subgoal_file dfg mode ctxt negs user_thms n, timeLimit))))] n thm) handle (Fail _) => Seq.empty;
+fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms i st =
+  (EVERY'
+   [rtac ccontr,
+    ObjectLogic.atomize_prems_tac,
+    Meson.skolemize_tac,
+    METAHYPS (fn negs =>
+      HEADGOAL (Tactic.rtac
+        (res_atp_oracle (ProofContext.theory_of ctxt)
+          (ResAtp.write_subgoal_file dfg mode ctxt negs user_thms i, timeLimit))))] i st) handle Fail _ => Seq.empty;
+
 
 (* vampire, eprover and spass tactics *)
 
@@ -34,16 +50,20 @@
 
 fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.time_limit) st;
 
-val ResAtps_setup =
-  Method.add_methods 
-    [("vampireF", ResAtp.atp_method vampireF_tac, "Vampire for FOL problems"),
-     ("eproverF", ResAtp.atp_method eproverF_tac, "E prover for FOL problems"),
-     ("vampireH", ResAtp.atp_method vampireH_tac, "Vampire for HOL problems"),
-     ("eproverH", ResAtp.atp_method eproverH_tac, "E prover for HOL problems"),
-     ("eprover", ResAtp.atp_method eprover_tac, "E prover for FOL and HOL problems"),
-     ("vampire", ResAtp.atp_method vampire_tac, "Vampire for FOL and HOL problems"),
-     ("spassF", ResAtp.atp_method spassF_tac, "SPASS for FOL problems"),
-     ("spassH", ResAtp.atp_method spassH_tac, "SPASS for HOL problems"),
-     ("spass", ResAtp.atp_method spass_tac, "SPASS for FOL and HOL problems")];
+
+fun atp_method tac =
+  Method.thms_ctxt_args (fn ths => fn ctxt => Method.SIMPLE_METHOD' (tac ctxt ths));
 
-end
+val setup =
+  Method.add_methods
+    [("vampireF", atp_method vampireF_tac, "Vampire for FOL problems"),
+     ("eproverF", atp_method eproverF_tac, "E prover for FOL problems"),
+     ("vampireH", atp_method vampireH_tac, "Vampire for HOL problems"),
+     ("eproverH", atp_method eproverH_tac, "E prover for HOL problems"),
+     ("eprover", atp_method eprover_tac, "E prover for FOL and HOL problems"),
+     ("vampire", atp_method vampire_tac, "Vampire for FOL and HOL problems"),
+     ("spassF", atp_method spassF_tac, "SPASS for FOL problems"),
+     ("spassH", atp_method spassH_tac, "SPASS for HOL problems"),
+     ("spass", atp_method spass_tac, "SPASS for FOL and HOL problems")];
+
+end;