diff -r 75a48dc4383e -r baa7a1e57f4a src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Tue Feb 25 20:57:57 2014 +0100
+++ b/src/Pure/Thy/latex.ML	Tue Feb 25 21:32:26 2014 +0100
@@ -178,7 +178,7 @@
   in (output_symbols syms, Symbol.length syms) end;
 
 fun latex_markup (s, _) =
-  if s = Markup.keyword1N then ("\\isacommand{", "}")
+  if s = Markup.commandN orelse s = Markup.keyword1N then ("\\isacommand{", "}")
   else if s = Markup.keyword2N then ("\\isakeyword{", "}")
   else Markup.no_output;