author | blanchet |
Tue, 01 Feb 2022 17:11:26 +0100 | |
changeset 75056 | 04a4881ff0fd |
parent 75055 | c84a20e9b00f |
child 75057 | 79b4e711d6a2 |
--- 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