text_of Malformed: explode with spaces -- Output.output/escape ineffective by default;

--- 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);