# HG changeset patch
# User wenzelm
# Date 1223055318 -7200
# Node ID b54665917c8dff52307689e2edd9e0d41801c39b
# Parent  4ed9239b09c1c9ea38fbd95aa389595cfcd73526
operate on Proof.state, not Toplevel.state;
moved setup to ATP_Linkup.thy;

diff -r 4ed9239b09c1 -r b54665917c8d src/HOL/Tools/atp_thread.ML
--- a/src/HOL/Tools/atp_thread.ML	Fri Oct 03 19:35:17 2008 +0200
+++ b/src/HOL/Tools/atp_thread.ML	Fri Oct 03 19:35:18 2008 +0200
@@ -14,26 +14,26 @@
     string ->
     (string * int -> bool) ->
     (string * string vector * Proof.context * Thm.thm * int -> string) ->
-    Toplevel.state -> Thread.thread * string
+    Proof.state -> Thread.thread * string
   (* settings for writing problemfiles *)
   val destdir: string ref
   val problem_name: string ref
   (* provers as functions returning threads *)
-  val tptp_prover_filter_opts_full: int -> bool -> bool -> string -> Toplevel.state -> (Thread.thread * string)
-  val tptp_prover_filter_opts: int -> bool -> string -> Toplevel.state -> (Thread.thread * string)
-  val full_prover_filter_opts: int -> bool -> string -> Toplevel.state -> (Thread.thread * string)
-  val tptp_prover: string -> Toplevel.state -> (Thread.thread * string)
-  val full_prover: string -> Toplevel.state -> (Thread.thread * string)  val spass_filter_opts: int -> bool -> Toplevel.state -> (Thread.thread * string)
-  val eprover_filter_opts: int -> bool -> Toplevel.state -> (Thread.thread * string)
-  val eprover_filter_opts_full: int -> bool -> Toplevel.state -> (Thread.thread * string)
-  val vampire_filter_opts: int -> bool -> Toplevel.state -> (Thread.thread * string)
-  val vampire_filter_opts_full: int -> bool -> Toplevel.state -> (Thread.thread * string)
-  val spass: Toplevel.state -> (Thread.thread * string)
-  val eprover: Toplevel.state -> (Thread.thread * string)
-  val eprover_full: Toplevel.state -> (Thread.thread * string)
-  val vampire: Toplevel.state -> (Thread.thread * string)
-  val vampire_full: Toplevel.state -> (Thread.thread * string)
-  val setup: theory -> theory
+  val tptp_prover_filter_opts_full: int -> bool -> bool -> string -> Proof.state -> (Thread.thread * string)
+  val tptp_prover_filter_opts: int -> bool -> string -> Proof.state -> (Thread.thread * string)
+  val full_prover_filter_opts: int -> bool -> string -> Proof.state -> (Thread.thread * string)
+  val tptp_prover: string -> Proof.state -> (Thread.thread * string)
+  val full_prover: string -> Proof.state -> (Thread.thread * string)
+  val spass_filter_opts: int -> bool -> Proof.state -> (Thread.thread * string)
+  val eprover_filter_opts: int -> bool -> Proof.state -> (Thread.thread * string)
+  val eprover_filter_opts_full: int -> bool -> Proof.state -> (Thread.thread * string)
+  val vampire_filter_opts: int -> bool -> Proof.state -> (Thread.thread * string)
+  val vampire_filter_opts_full: int -> bool -> Proof.state -> (Thread.thread * string)
+  val spass: Proof.state -> (Thread.thread * string)
+  val eprover: Proof.state -> (Thread.thread * string)
+  val eprover_full: Proof.state -> (Thread.thread * string)
+  val vampire: Proof.state -> (Thread.thread * string)
+  val vampire_full: Proof.state -> (Thread.thread * string)
 end;
 
 structure AtpThread : ATP_THREAD =
@@ -71,7 +71,7 @@
       (*creating description from provername and subgoal*)
     val call::path = rev (String.tokens (fn c => c = #"/") command)
     val name::options = String.tokens (fn c => c = #" ") call
-    val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state)
+    val (ctxt, (chain_ths, goal)) = Proof.get_goal state
     val description = "External prover '" ^ name ^ "' for Subgoal " ^ Int.toString subgoalno
       ^ ":\n" ^ Display.string_of_cterm (List.nth(cprems_of goal, subgoalno-1))
       (* path to unique problemfile *)
@@ -180,20 +180,4 @@
 
   (*TODO: Thread running some selected or recommended provers of "System On TPTP" *)
 
-
-
-  fun add_prover name prover_fun = AtpManager.Provers.map (Symtab.update (name, prover_fun))
-
-    (* include 'original' provers and provers with structured output *)
-  val setup =
-    (* original setups *)
-    add_prover "spass" spass #>
-    add_prover "vampire" vampire #>
-    add_prover "e" eprover #>
-    (* provers with stuctured output *)
-    add_prover "vampire_full" vampire_full #>
-    add_prover "e_full" eprover_full #>
-    (* on some problems better results *)
-    add_prover "spass_no_tc" (spass_filter_opts 40 false);
-
 end;