src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 80820 db114ec720cb
parent 80809 4a64fc4d1cde
child 80874 9af593e9e454
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Sep 06 20:31:20 2024 +0200
@@ -165,7 +165,7 @@
    expect : string}
 
 fun string_of_params (params : params) =
-  YXML.content_of (ML_Pretty.string_of (ML_system_pretty (params, 100)))
+  Protocol_Message.clean_output (ML_Pretty.string_of (ML_system_pretty (params, 100)))
 
 fun maybe_filter_out_induction_rules induction_rules : fact list -> fact list =
   induction_rules = Exclude ?