--- a/src/HOL/Tools/atp_manager.ML Tue Jan 20 18:12:06 2009 +0100
+++ b/src/HOL/Tools/atp_manager.ML Tue Jan 20 20:58:08 2009 +0100
@@ -19,7 +19,7 @@
val kill: unit -> unit
val info: unit -> unit
val messages: int option -> unit
- type prover = int -> Proof.state -> bool * string
+ type prover = int -> int -> Proof.state -> bool * string
val add_prover: string -> prover -> theory -> theory
val print_provers: theory -> unit
val sledgehammer: string list -> Proof.state -> unit
@@ -264,7 +264,7 @@
(* named provers *)
-type prover = int -> Proof.state -> bool * string;
+type prover = int -> int -> Proof.state -> bool * string;
fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
@@ -300,7 +300,7 @@
val _ = SimpleThread.fork true (fn () =>
let
val _ = register birthtime deadtime (Thread.self (), desc)
- val result = prover i proof_state
+ val result = prover (get_timeout ()) i proof_state
handle ResHolClause.TOO_TRIVIAL
=> (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
| ERROR msg