# HG changeset patch
# User wenzelm
# Date 1219876391 -7200
# Node ID 33050286e65d4850b9433fba18a23e412e28f1ee
# Parent  f03b5856f2865307d6a2aa5da7321d4fa440e0ec
text_of Malformed: explode with spaces -- Output.output/escape ineffective by default;

diff -r f03b5856f286 -r 33050286e65d src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Thu Aug 28 00:33:09 2008 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Thu Aug 28 00:33:11 2008 +0200
@@ -200,7 +200,7 @@
   | AltString => x |> enclose "`" "`" o escape "`"
   | Verbatim => x |> enclose "{*" "*}"
   | Comment => x |> enclose "(*" "*)"
-  | Malformed => Output.escape (translate_string Output.output x)
+  | Malformed => space_implode " " (explode x)
   | Sync => ""
   | EOF => ""
   | _ => x);