# HG changeset patch
# User blanchet
# Date 1643731886 -3600
# Node ID 04a4881ff0fd66266980d139b5d111aae9dffbbd
# Parent  c84a20e9b00f826bc0057226b0c7ceb7b2755315
propagate right result when enough proofs have been found

diff -r c84a20e9b00f -r 04a4881ff0fd src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Feb 01 16:16:50 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Feb 01 17:11:26 2022 +0100
@@ -445,7 +445,7 @@
                    if Synchronized.value found_proofs < max_proofs then
                      launch problem slice prover
                    else
-                     (SH_Unknown, ""))
+                     (SH_None, ""))
                  prover_slices
                |> max_outcome)
           end