# HG changeset patch
# User wenzelm
# Date 1733824366 -3600
# Node ID a1ad3d1761fe54d53189ae05cae184875174e80d
# Parent  f207acb03ccb39d5c08f3a5948968f26526aca24
tuned;

diff -r f207acb03ccb -r a1ad3d1761fe src/Pure/General/latex.ML
--- a/src/Pure/General/latex.ML	Sun Dec 08 20:13:40 2024 +0100
+++ b/src/Pure/General/latex.ML	Tue Dec 10 10:52:46 2024 +0100
@@ -243,9 +243,10 @@
 
 local
 
-val command_markup = YXML.output_markup (Markup.latex_macro "isacommand");
-val keyword_markup = YXML.output_markup (Markup.latex_macro "isakeyword");
-val indent_markup = YXML.output_markup (Markup.latex_macro "isaindent");
+val macro_markup = YXML.output_markup o Markup.latex_macro;
+val command_markup = macro_markup "isacommand";
+val keyword_markup = macro_markup "isakeyword";
+val indent_markup = macro_markup "isaindent";
 
 fun latex_markup (s, _: Properties.T) =
   if member (op =) [Markup.commandN, Markup.keyword1N, Markup.keyword3N] s then command_markup