src/Pure/General/latex.ML
changeset 81628 e5be995d21f0
parent 81587 68dc8ffc94c2
child 81682 2f98e3c4592c
--- a/src/Pure/General/latex.ML	Wed Dec 18 12:49:42 2024 +0100
+++ b/src/Pure/General/latex.ML	Wed Dec 18 13:49:55 2024 +0100
@@ -247,10 +247,10 @@
 val markup_indent = markup_macro "isaindent";
 val markup_latex =
  Symtab.make
-  [(Markup.commandN, markup_macro "isacommand"),
-   (Markup.keyword1N, markup_macro "isacommand"),
-   (Markup.keyword2N, markup_macro "isakeyword"),
-   (Markup.keyword3N, markup_macro "isacommand"),
+  [(Markup.commandN, markup_macro "isakeywordONE"),
+   (Markup.keyword1N, markup_macro "isakeywordONE"),
+   (Markup.keyword2N, markup_macro "isakeywordTWO"),
+   (Markup.keyword3N, markup_macro "isakeywordTHREE"),
    (Markup.tclassN, markup_macro "isatclass"),
    (Markup.tconstN, markup_macro "isatconst"),
    (Markup.tfreeN, markup_macro "isatfree"),