src/HOL/Tools/atp_manager.ML

   val get_timeout: unit -> int
   val set_timeout: int -> unit
   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
 end;
 

 
 (** The Sledgehammer **)
 
 (* 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);
 
 structure Provers = TheoryDataFun
 (

           "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
             Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))
         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
                 => (false, "Error: " ^ msg)
             val _ = unregister result (Thread.self ())

       Toplevel.keep ((sledgehammer names) o Toplevel.proof_of)));
 
 end;
 
 end;
+