src/HOL/Tools/Sledgehammer/sledgehammer.ML

               (learn chained_thms;
                Par_List.map (fn (prover, slice) =>
                    if Synchronized.value found_proofs < max_proofs then
                      launch problem slice prover
                    else
-                     (SH_Unknown, ""))
+                     (SH_None, ""))
                  prover_slices
                |> max_outcome)
           end
       in
         (launch_provers ()