src/Pure/Thy/latex.ML
changeset 23703 1b6a2c119151
parent 23621 e070a6ab1891
child 27344 d44490b06190
     1.1 --- a/src/Pure/Thy/latex.ML	Tue Jul 10 16:45:05 2007 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Tue Jul 10 16:45:06 2007 +0200
     1.3 @@ -176,6 +176,7 @@
     1.4    | latex_indent s _ = enclose "\\isaindent{" "}" s;
     1.5  
     1.6  val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
     1.7 -val _ = Pretty.add_mode latexN latex_indent latex_markup;
     1.8 +val _ = Markup.add_mode latexN latex_markup;
     1.9 +val _ = Pretty.add_mode latexN latex_indent;
    1.10  
    1.11  end;