changeset 80820 | db114ec720cb |
parent 80636 | 4041e7c8059d |
child 81254 | d3c0734059ee |
--- a/src/HOL/Tools/ATP/atp_util.ML Fri Sep 06 19:17:29 2024 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Fri Sep 06 20:31:20 2024 +0200 @@ -143,7 +143,7 @@ val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode fun maybe_quote ctxt y = let - val s = YXML.content_of y + val s = Protocol_Message.clean_output y val is_literal = Keyword.is_literal (Thy_Header.get_keywords' ctxt) val q = if Config.get ctxt proof_cartouches then cartouche else quote in