--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Thu Oct 24 22:05:57 2024 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri Oct 25 15:31:58 2024 +0200
@@ -196,8 +196,8 @@
preplay_results
|> map
(fn (meth, (play_outcome, used_facts)) =>
- "Preplay: " ^
- Sledgehammer_Proof_Methods.string_of_proof_method (map fst used_facts) meth ^
+ "Preplay: " ^ Sledgehammer_Proof_Methods.string_of_proof_method
+ (map (ATP_Util.content_of_pretty o fst) used_facts) meth ^
" (" ^ Sledgehammer_Proof_Methods.string_of_play_outcome play_outcome ^ ")")
|> cat_lines
else
@@ -211,7 +211,7 @@
(case time_prover of NONE => "" | SOME ms => ", ATP " ^ string_of_int ms ^ "ms") ^
") [" ^ prover_name ^ "]: "
in
- (sledgehamer_outcome, triv_str ^ outcome_msg ^ msg ^
+ (sledgehamer_outcome, triv_str ^ outcome_msg ^ Protocol_Message.clean_output msg ^
(if exhaustive_preplay_msg = "" then "" else ("\n" ^ exhaustive_preplay_msg)),
change_data #> inc_sh_time_isa cpu_time)
end