src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML

 fun maybe_filter_out_induction_rules induction_rules : fact list -> fact list =
     induction_rules = Exclude ?
       filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false)
 
 fun slice_timeout slices timeout =
-  Time.toReal timeout * Real.fromInt (Multithreading.max_threads ()) / Real.fromInt slices
-  |> seconds
+  let
+    val max_threads = Multithreading.max_threads ()
+    val batches = (slices + max_threads - 1) div max_threads
+  in
+    seconds (Time.toReal timeout / Real.fromInt batches)
+  end
 
 type prover_problem =
   {comment : string,
    state : Proof.state,
    goal : thm,

 
 fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
 
 fun proof_banner mode prover_name =
   (case mode of
-    Auto_Try => "Auto Sledgehammer (" ^ prover_name ^ ") found a proof"
-  | Try => "Sledgehammer (" ^ prover_name ^ ") found a proof"
-  | _ => "Try this")
+    Auto_Try => "Auto Sledgehammer (" ^ prover_name ^ ") found a proof: "
+  | Try => "Sledgehammer (" ^ prover_name ^ ") found a proof: "
+  | _ => "")
 
 fun bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types desperate_lam_trans =
   let
     val try0_methodss =
       if try0 then