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"