# HG changeset patch
# User aspinall
# Date 1096361014 -7200
# Node ID b62f72ea3bb031cdcbac81af258cc320ea751b36
# Parent  09271a87fbf03930a1205d1d01520d7d68917a0b
Fix to unparse to not double-escape backslash

diff -r 09271a87fbf0 -r b62f72ea3bb0 src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Mon Sep 27 16:03:16 2004 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Tue Sep 28 10:43:34 2004 +0200
@@ -142,7 +142,7 @@
 
 fun unparse (Token (_, (kind, x))) =
   (case kind of
-    String => x |> translate_string (fn "\"" => "\\\"" | "\\" => "\\\\" | c => c) |> quote
+    String => x |> quote
   | Verbatim => x |> enclose "{*" "*}"
   | Comment => x |> enclose "(*" "*)"
   | _ => x);