changeset 80866 | 8c67b14fdd48 |
parent 80820 | db114ec720cb |
child 80874 | 9af593e9e454 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Sep 11 23:07:18 2024 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Sep 11 23:26:25 2024 +0200 @@ -131,7 +131,8 @@ 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) + #> *) Syntax.pretty_term ctxt + #> Pretty.pure_string_of #> Protocol_Message.clean_output #> simplify_spaces