# HG changeset patch
# User blanchet
# Date 1272384101 -7200
# Node ID 1281be23bd23d4cb6a52009170144978bb0fa7a9
# Parent  af99c98121d6e00d9e2c2ad248777d91c2f4ef10
added total goal count as argument + message when killing ATPs

diff -r af99c98121d6 -r 1281be23bd23 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Apr 27 17:44:33 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Apr 27 18:01:41 2010 +0200
@@ -58,7 +58,7 @@
   val get_prover: theory -> string -> prover
   val available_atps: theory -> unit
   val start_prover_thread:
-    params -> Time.time -> Time.time -> int -> relevance_override
+    params -> Time.time -> Time.time -> int -> int -> relevance_override
     -> (string -> minimize_command) -> Proof.state -> string -> unit
 end;
 
@@ -266,6 +266,8 @@
     let
       val killing = map (fn (th, (_, _, desc)) => (th, (Time.now (), desc))) active;
       val state' = make_state manager timeout_heap [] (killing @ cancelling) messages store;
+      val _ = if null active then ()
+              else priority "Killed active Sledgehammer threads."
     in state' end);
 
 
@@ -336,12 +338,11 @@
 
 (* start prover thread *)
 
-fun start_prover_thread (params as {timeout, ...}) birth_time death_time i
+fun start_prover_thread (params as {timeout, ...}) birth_time death_time i n
                         relevance_override minimize_command proof_state name =
   let
     val prover = get_prover (Proof.theory_of proof_state) name
     val {context = ctxt, facts, goal} = Proof.goal proof_state;
-    val n = Logic.count_prems (prop_of goal)
     val desc =
       "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
       Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));