--- 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 *)
--- 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;
--- a/src/Pure/proof_general.ML Sun Jun 20 09:26:29 2004 +0200
+++ b/src/Pure/proof_general.ML Sun Jun 20 09:26:48 2004 +0200
@@ -60,7 +60,7 @@
in
fun setup_xsymbols_output () = Output.add_mode proof_generalN
- (pgml_output o xsymbols_output, Symbol.default_indent, Symbol.default_raw);
+ (pgml_output o xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
end;