src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
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