changeset 14561 | c53396af770e |
parent 14557 | 31ae4a47267c |
child 14566 | 0b60b2edce03 |
1.1 --- a/src/Pure/proof_general.ML Wed Apr 14 11:44:57 2004 +0200 1.2 +++ b/src/Pure/proof_general.ML Wed Apr 14 12:19:16 2004 +0200 1.3 @@ -48,7 +48,7 @@ 1.4 fun xsymbols_output s = 1.5 if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then 1.6 let val syms = Symbol.explode s 1.7 - in (s, real (Symbol.length syms)) end 1.8 + in (implode (map Symbol.escape syms), real (Symbol.length syms)) end 1.9 else (s, real (size s)); 1.10 1.11 fun pgml_output (s, len) =