diff -r ce3a0d2c9aa7 -r cf9becb6403f src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Sat Mar 09 11:35:32 2024 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Sat Mar 09 11:51:52 2024 +0100
@@ -144,12 +144,12 @@
 fun maybe_quote ctxt y =
   let
     val s = YXML.content_of y
-    val is_literal = (Keyword.is_literal o Thy_Header.get_keywords') ctxt
-    val gen_quote = if Config.get ctxt proof_cartouches then cartouche else quote
+    val is_literal = Keyword.is_literal (Thy_Header.get_keywords' ctxt)
+    val q = if Config.get ctxt proof_cartouches then cartouche else quote
   in
     y |> ((not (is_long_identifier (unquote_tvar s)) andalso
            not (is_long_identifier (unquery_var s))) orelse
-           is_literal s) ? gen_quote
+           is_literal s) ? q
   end
 
 fun string_of_ext_time (plus, time) =