| changeset 14973 | 0613f64653b7 |
| parent 14839 | c994f1c57fc7 |
| child 14981 | e73f8140af78 |
--- a/src/Pure/Thy/html.ML Sun Jun 20 09:26:29 2004 +0200 +++ b/src/Pure/Thy/html.ML Sun Jun 20 09:26:48 2004 +0200 @@ -238,7 +238,7 @@ end; -val _ = Output.add_mode htmlN (output_width, Symbol.default_indent, Symbol.default_raw); +val _ = Output.add_mode htmlN (output_width, Symbol.default_indent, Symbol.encode_raw); (* token translations *)