# HG changeset patch
# User immler@in.tum.de
# Date 1237045825 -3600
# Node ID 0dd8dfe424cfd4238706e285f48ddc7a1e3d4bd4
# Parent  07b4f050e4df2e9044536608b78b57d650ef54d0
use goal instead of Proof State

diff -r 07b4f050e4df -r 0dd8dfe424cf src/HOL/Tools/atp_manager.ML
--- a/src/HOL/Tools/atp_manager.ML	Sat Mar 14 16:46:23 2009 +0100
+++ b/src/HOL/Tools/atp_manager.ML	Sat Mar 14 16:50:25 2009 +0100
@@ -19,7 +19,7 @@
   val kill: unit -> unit
   val info: unit -> unit
   val messages: int option -> unit
-  type prover = int -> int -> Proof.state -> bool * string
+  type prover = int -> int -> Proof.context * (thm list * thm) -> bool * string 
   val add_prover: string -> prover -> theory -> theory
   val print_provers: theory -> unit
   val sledgehammer: string list -> Proof.state -> unit
@@ -271,7 +271,7 @@
 
 (* named provers *)
 
-type prover = int -> int -> Proof.state -> bool * string;
+type prover = int -> int -> Proof.context * (thm list * thm) -> bool * string;
 
 fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
 
@@ -307,7 +307,7 @@
         val _ = SimpleThread.fork true (fn () =>
           let
             val _ = register birthtime deadtime (Thread.self (), desc)
-            val result = prover (get_timeout ()) i proof_state
+            val result = prover (get_timeout ()) i (Proof.get_goal proof_state) 
               handle ResHolClause.TOO_TRIVIAL
                 => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
               | ERROR msg
@@ -360,3 +360,4 @@
 end;
 
 end;
+
diff -r 07b4f050e4df -r 0dd8dfe424cf src/HOL/Tools/atp_wrapper.ML
--- a/src/HOL/Tools/atp_wrapper.ML	Sat Mar 14 16:46:23 2009 +0100
+++ b/src/HOL/Tools/atp_wrapper.ML	Sat Mar 14 16:50:25 2009 +0100
@@ -47,7 +47,7 @@
 
 (* basic template *)
 
-fun external_prover axiom_clauses write_problem_file (cmd, args) find_failure produce_answer timeout subgoalno state =
+fun external_prover axiom_clauses write_problem_file (cmd, args) find_failure produce_answer timeout subgoalno goal =
   let
     (* path to unique problem file *)
     val destdir' = ! destdir
@@ -61,12 +61,12 @@
       end
 
     (* write out problem file and call prover *)
-    val (ctxt, (chain_ths, goal)) = Proof.get_goal state
+    val (ctxt, (chain_ths, th)) = goal
     val thy = ProofContext.theory_of ctxt
     val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
     val probfile = prob_pathname subgoalno
     val fname = File.platform_path probfile
-    val thm_names = write_problem_file probfile goal subgoalno axiom_clauses thy
+    val thm_names = write_problem_file probfile th subgoalno axiom_clauses thy
     val cmdline =
       if File.exists cmd then File.shell_path cmd ^ " " ^ args
       else error ("Bad executable: " ^ Path.implode cmd)
@@ -81,7 +81,7 @@
     val message =
       if isSome failure then "Proof attempt failed."
       else if rc <> 0 then "Proof attempt failed: " ^ proof
-      else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
+      else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, th, subgoalno)
 
     val _ = if isSome failure
       then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof)
@@ -97,14 +97,14 @@
 
 (* generic TPTP-based provers *)
 
-fun tptp_prover_opts_full max_new theory_const full command timeout n state =
+fun tptp_prover_opts_full max_new theory_const full command timeout n goal =
   external_prover
-    (ResAtp.get_relevant max_new theory_const (Proof.get_goal state) n)
+    (ResAtp.get_relevant max_new theory_const goal n)
     (ResAtp.write_problem_file false)
     command
     ResReconstruct.find_failure_e_vamp_spass
     (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
-    timeout n state;
+    timeout n goal;
 
 (*arbitrary ATP with TPTP input/output and problemfile as last argument*)
 fun tptp_prover_opts max_new theory_const =
@@ -161,14 +161,14 @@
 
 (* SPASS *)
 
-fun spass_opts max_new theory_const timeout n state = external_prover
-  (ResAtp.get_relevant max_new theory_const (Proof.get_goal state) n)
+fun spass_opts max_new theory_const timeout n goal = external_prover
+  (ResAtp.get_relevant max_new theory_const goal n)
   (ResAtp.write_problem_file true)
   (Path.explode "$SPASS_HOME/SPASS",
     "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
   ResReconstruct.find_failure_e_vamp_spass
   ResReconstruct.lemma_list_dfg
-  timeout n state;
+  timeout n goal;
 
 val spass = spass_opts 40 true;