# HG changeset patch
# User schirmer
# Date 1082014392 -7200
# Node ID 03a827b7dbe8df55fdf79177525782ccfaecc6fb
# Parent  0b60b2edce03db83059b3bea2b14d8d1a8017d2b
bugfix in xsymbols_output

diff -r 0b60b2edce03 -r 03a827b7dbe8 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Wed Apr 14 15:09:51 2004 +0200
+++ b/src/Pure/proof_general.ML	Thu Apr 15 09:33:12 2004 +0200
@@ -48,7 +48,7 @@
 fun xsymbols_output s =
   if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
     let val syms = Symbol.explode s
-    in (implode (map Symbol.escape syms), real (Symbol.length syms)) end
+    in (implode (map (fn "\\" => "\\\\" | c => c) syms), real (Symbol.length syms)) end
   else (s, real (size s));
 
 fun pgml_output (s, len) =