run all provers in blocking mode, even if a proof was already found -- this behavior is less confusing to the user

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Feb 10 16:05:33 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Feb 10 16:15:43 2011 +0100
@@ -238,16 +238,16 @@
                      else
                        ())
         end
-      fun launch_atps (accum as (success, _)) =
-        if success orelse null atps then
+      fun launch_atps accum =
+        if null atps then
           accum
         else
           launch_provers state
               (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
               (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst))
               (K (K NONE)) atps
-      fun launch_smts (accum as (success, _)) =
-        if success orelse null smts then
+      fun launch_smts accum =
+        if null smts then
           accum
         else
           let