# HG changeset patch
# User blanchet
# Date 1297350943 -3600
# Node ID e590971528b2d354c94ee72129a338fc0ad5eaa1
# Parent  4b3edd6a375d3a5e1dc51537140073c0332fe94a
run all provers in blocking mode, even if a proof was already found -- this behavior is less confusing to the user

diff -r 4b3edd6a375d -r e590971528b2 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- 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