--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Wed Sep 11 23:07:18 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Wed Sep 11 23:26:25 2024 +0200
@@ -405,7 +405,8 @@
(s ^ (term
|> singleton (Syntax.uncheck_terms ctxt)
|> annotate_types_in_term ctxt
- |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
+ |> Syntax.unparse_term ctxt
+ |> Pretty.pure_string_of
|> simplify_spaces
|> maybe_quote ctxt),
ctxt |> perhaps (try (Proof_Context.augment term)))
@@ -425,7 +426,7 @@
fun of_free (s, T) =
Thy_Header.print_name' ctxt s ^ " :: " ^
- maybe_quote ctxt (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T))
+ maybe_quote ctxt (simplify_spaces (Pretty.pure_string_of (Syntax.pretty_typ ctxt T)))
fun add_frees xs (s, ctxt) =
(s ^ space_implode " and " (map of_free xs), ctxt |> fold Proof_Context.augment (map Free xs))