src/Pure/proof_general.ML
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) =