# HG changeset patch
# User desharna
# Date 1741078511 -3600
# Node ID 067dac998c59a35984aded0542dec49c19eebede
# Parent  cbe937aa5e90c85dc9e0bff20eee647b5dcb7d28
removed misleading output of Mirabelle's sledgehammer action

diff -r cbe937aa5e90 -r 067dac998c59 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- 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)),