# HG changeset patch
# User blanchet
# Date 1275656977 -7200
# Node ID bf5d936bb985ee3c410742e9c85e9c0cb8311332
# Parent  c2a44bc874f9d106e2772b87ee242f1f64ccd72f
kill active Sledgehammer threads when running minimize, to avoid confusing the user with too much output

diff -r c2a44bc874f9 -r bf5d936bb985 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 04 15:08:50 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 04 15:09:37 2010 +0200
@@ -226,7 +226,7 @@
       let
         val birth_time = Time.now ()
         val death_time = Time.+ (birth_time, timeout)
-        val _ = kill_atps ()  (* race w.r.t. other Sledgehammer invocations *)
+        val _ = kill_atps ()
         val _ = priority "Sledgehammering..."
         val _ = app (start_prover_thread params birth_time death_time i n
                                          relevance_override minimize_command
@@ -249,8 +249,10 @@
   in
     case subgoal_count state of
       0 => priority "No subgoal!"
-    | n => priority (#2 (minimize_theorems (get_params thy override_params) i n
-                                           state name_thms_pairs))
+    | n =>
+      (kill_atps ();
+       priority (#2 (minimize_theorems (get_params thy override_params) i n
+                                       state name_thms_pairs)))
   end
 
 val sledgehammerN = "sledgehammer"