changeset 55750 | baa7a1e57f4a |
parent 55744 | 4a4e5686e091 |
child 55828 | 42ac3cfb89f6 |
--- 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;