src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML

--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Wed Dec 15 23:18:41 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Fri Dec 17 09:51:37 2021 +0100
@@ -536,6 +536,8 @@
     val data = Synchronized.var "Mirabelle_Sledgehammer.data" empty_data
     val change_data = Synchronized.change data
 
+    val init_msg = "Params for sledgehammer: " ^ Sledgehammer_Prover.string_of_params params
+
     fun run_action ({theory_index, name, pos, pre, ...} : Mirabelle.command) =
       let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
         if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then
@@ -561,7 +563,7 @@
       end
 
     fun finalize () = log_data (Synchronized.value data)
-  in {run_action = run_action, finalize = finalize} end
+  in (init_msg, {run_action = run_action, finalize = finalize}) end
 
 val () = Mirabelle.register_action "sledgehammer" make_action