src/Pure/Thy/latex.ML
changeset 55744 4a4e5686e091
parent 55033 8e8243975860
child 55750 baa7a1e57f4a
     1.1 --- a/src/Pure/Thy/latex.ML	Tue Feb 25 14:56:58 2014 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Tue Feb 25 17:03:55 2014 +0100
     1.3 @@ -178,10 +178,8 @@
     1.4    in (output_symbols syms, Symbol.length syms) end;
     1.5  
     1.6  fun latex_markup (s, _) =
     1.7 -  if s = Markup.commandN orelse s = Markup.keyword1N
     1.8 -    then ("\\isacommand{", "}")
     1.9 -  else if s = Markup.keywordN orelse s = Markup.keyword2N
    1.10 -    then ("\\isakeyword{", "}")
    1.11 +  if s = Markup.keyword1N then ("\\isacommand{", "}")
    1.12 +  else if s = Markup.keyword2N then ("\\isakeyword{", "}")
    1.13    else Markup.no_output;
    1.14  
    1.15  fun latex_indent "" _ = ""