| changeset 14973 | 0613f64653b7 |
| parent 14924 | 2be4cbe27a27 |
| child 14981 | e73f8140af78 |
--- a/src/Pure/Thy/latex.ML Sun Jun 20 09:26:29 2004 +0200 +++ b/src/Pure/Thy/latex.ML Sun Jun 20 09:26:48 2004 +0200 @@ -155,7 +155,7 @@ fun latex_indent "" = "" | latex_indent s = enclose "\\isaindent{" "}" s; -val _ = Output.add_mode latexN (latex_output, latex_indent o #1, Symbol.default_raw); +val _ = Output.add_mode latexN (latex_output, latex_indent o #1, Symbol.encode_raw); end;