src/Pure/Thy/latex.ML

--- a/src/Pure/Thy/latex.ML	Fri Jan 02 22:52:42 2009 +0100
+++ b/src/Pure/Thy/latex.ML	Fri Jan 02 22:54:04 2009 +0100
@@ -174,7 +174,7 @@
 fun latex_markup (s, _) =
   if s = Markup.keywordN then ("\\isakeyword{", "}")
   else if s = Markup.commandN then ("\\isacommand{", "}")
-  else ("", "");
+  else Markup.no_output;
 
 fun latex_indent "" _ = ""
   | latex_indent s _ = enclose "\\isaindent{" "}" s;