simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;

--- a/src/Pure/Isar/token.ML	Sat Nov 13 20:49:02 2010 +0100
+++ b/src/Pure/Isar/token.ML	Sat Nov 13 21:01:03 2010 +0100
@@ -200,7 +200,6 @@
   | AltString => x |> enclose "`" "`" o escape "`"
   | Verbatim => x |> enclose "{*" "*}"
   | Comment => x |> enclose "(*" "*)"
-  | Malformed => space_implode " " (explode x)
   | Sync => ""
   | EOF => ""
   | _ => x);