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