changeset 14561 | c53396af770e |
parent 14557 | 31ae4a47267c |
child 14566 | 0b60b2edce03 |
--- a/src/Pure/proof_general.ML Wed Apr 14 11:44:57 2004 +0200 +++ b/src/Pure/proof_general.ML Wed Apr 14 12:19:16 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 (s, real (Symbol.length syms)) end + in (implode (map Symbol.escape syms), real (Symbol.length syms)) end else (s, real (size s)); fun pgml_output (s, len) =