author | schirmer |
Thu, 15 Apr 2004 09:33:12 +0200 | |
changeset 14567 | 03a827b7dbe8 |
parent 14566 | 0b60b2edce03 |
child 14568 | 1acde8c39179 |
--- 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) =