src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 80820 db114ec720cb
parent 80306 c2537860ccf8
child 80866 8c67b14fdd48
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Sep 06 20:31:20 2024 +0200
@@ -132,7 +132,7 @@
 fun hackish_string_of_term ctxt =
   (* FIXME: map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t)
   #> *) Print_Mode.setmp [] (Syntax.string_of_term ctxt)
-  #> YXML.content_of
+  #> Protocol_Message.clean_output
   #> simplify_spaces
 
 val spying_version = "d"