--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Mon Mar 03 19:52:18 2025 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Tue Mar 04 09:55:11 2025 +0100
@@ -157,7 +157,7 @@
in
-fun run_sledgehammer (params as {provers, ...}) output_dir keep_probs keep_proofs
+fun run_sledgehammer params output_dir keep_probs keep_proofs
exhaustive_preplay thy_index trivial pos st =
let
val triv_str = if trivial then "[T] " else ""
@@ -176,7 +176,6 @@
end
else
NONE
- val prover_name = hd provers
val (sledgehamer_outcome, msg, cpu_time) = run_sh params keep pos st
val (time_prover, change_data, exhaustive_preplay_msg) =
(case sledgehamer_outcome of
@@ -208,8 +207,7 @@
| _ => (NONE, I, ""))
val outcome_msg =
"(SH " ^ string_of_int cpu_time ^ "ms" ^
- (case time_prover of NONE => "" | SOME ms => ", ATP " ^ string_of_int ms ^ "ms") ^
- ") [" ^ prover_name ^ "]: "
+ (case time_prover of NONE => "" | SOME ms => ", ATP " ^ string_of_int ms ^ "ms") ^ "): "
in
(sledgehamer_outcome, triv_str ^ outcome_msg ^ Protocol_Message.clean_output msg ^
(if exhaustive_preplay_msg = "" then "" else ("\n" ^ exhaustive_preplay_msg)),