# HG changeset patch
# User blanchet
# Date 1283359627 -7200
# Node ID d73a054e018c467a4a279b52addc3a27d68dc2fe
# Parent  8223d0f8f5cc40d2eb531805b197cbac5c64d168
only kill ATP threads in nonblocking mode

diff -r 8223d0f8f5cc -r d73a054e018c src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 01 18:42:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 01 18:47:07 2010 +0200
@@ -394,7 +394,7 @@
       let
         val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
         val thy = Proof.theory_of state
-        val _ = kill_atps ()
+        val _ = () |> not blocking ? kill_atps
         val _ = priority "Sledgehammering..."
         val (_, hyp_ts, concl_t) = strip_subgoal goal i
         val provers = map (`(get_prover thy)) atps