--- a/src/Pure/Thy/latex.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Thy/latex.ML Sun Nov 25 19:49:24 2012 +0100
@@ -178,9 +178,9 @@
in (output_symbols syms, Symbol.length syms) end;
fun latex_markup (s, _) =
- if s = Isabelle_Markup.commandN orelse s = Isabelle_Markup.keyword1N
+ if s = Markup.commandN orelse s = Markup.keyword1N
then ("\\isacommand{", "}")
- else if s = Isabelle_Markup.keywordN orelse s = Isabelle_Markup.keyword2N
+ else if s = Markup.keywordN orelse s = Markup.keyword2N
then ("\\isakeyword{", "}")
else Markup.no_output;