diff -r 2c787345c083 -r 2156a7392885 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Apr 16 15:49:46 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Apr 16 15:59:53 2010 +0200
@@ -223,7 +223,7 @@
         do
           (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
             |> these
-            |> List.app (unregister "Timed out.");
+            |> List.app (unregister "Interrupted (reached timeout)");
             print_new_messages ();
             (*give threads some time to respond to interrupt*)
             OS.Process.sleep min_wait_time)
@@ -325,7 +325,7 @@
 fun start_prover (params as {timeout, ...}) birth_time death_time i
                  relevance_override proof_state name =
   (case get_prover (Proof.theory_of proof_state) name of
-    NONE => warning ("Unknown ATP: " ^ quote name ^ ".")
+    NONE => warning ("Unknown ATP: " ^ quote name)
   | SOME prover =>
       let
         val {context = ctxt, facts, goal} = Proof.goal proof_state;
@@ -357,10 +357,7 @@
   let
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, timeout)
-    val _ =
-      (* RACE w.r.t. other invocations of Sledgehammer *)
-      if null (#active (Synchronized.value global_state)) then ()
-      else (kill_atps (); priority "Killed active Sledgehammer threads.")
+    val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *)
     val _ = priority "Sledgehammering..."
     val _ = List.app (start_prover params birth_time death_time i
                                    relevance_override proof_state) atps