| changeset 40531 | 8ede48c93c72 |
| parent 40525 | 14a2e686bdac |
| child 40627 | becf5d5187cc |
--- 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);