# HG changeset patch
# User wenzelm
# Date 1289678463 -3600
# Node ID 8ede48c93c7253d3e2618a251c0ee0cc085eaf7b
# Parent  f814863f391806f9884d5c0bea67a59db12d5d85
simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;

diff -r f814863f3918 -r 8ede48c93c72 src/Pure/Isar/token.ML
--- 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);