src/HOL/Tools/ATP/atp_util.ML
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