diff -r 84e886792536 -r db114ec720cb src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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"