# HG changeset patch
# User wenzelm
# Date 1087716408 -7200
# Node ID 0613f64653b7b2e005e0a3502acaa7ee50b05e32
# Parent  51f95648abadf649f03da9317a6cb15568095613
Symbol.encode_raw;

diff -r 51f95648abad -r 0613f64653b7 src/Pure/Thy/html.ML
--- 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 *)
diff -r 51f95648abad -r 0613f64653b7 src/Pure/Thy/latex.ML
--- 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;
diff -r 51f95648abad -r 0613f64653b7 src/Pure/proof_general.ML
--- 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;