changeset 80874 | 9af593e9e454 |
parent 80820 | db114ec720cb |
child 81362 | f586fdabe670 |
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Thu Sep 12 15:09:07 2024 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Thu Sep 12 19:46:08 2024 +0200 @@ -422,7 +422,7 @@ (*^ "\n" ^ string_of_reports reports*) in "mutant of " ^ Thm_Name.short thm_name ^ ":\n" ^ - Protocol_Message.clean_output (Syntax.string_of_term_global thy t) ^ "\n" ^ + Pretty.pure_string_of (Syntax.pretty_term_global thy t) ^ "\n" ^ space_implode "; " (map string_of_mtd_result results) end