1.1 --- a/src/Pure/Isar/token.ML	Sat Dec 04 14:59:25 2010 +0100
     1.2 +++ b/src/Pure/Isar/token.ML	Sat Dec 04 15:14:28 2010 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4    datatype kind =
     1.5      Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
     1.6      Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
     1.7 -    Malformed | Error of string | Sync | EOF
     1.8 +    Error of string | Sync | EOF
     1.9    datatype value =
    1.10      Text of string | Typ of typ | Term of term | Fact of thm list |
    1.11      Attribute of morphism -> attribute
    1.12 @@ -90,7 +90,7 @@
    1.13  datatype kind =
    1.14    Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
    1.15    Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
    1.16 -  Malformed | Error of string | Sync | EOF;
    1.17 +  Error of string | Sync | EOF;
    1.18  
    1.19  datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot;
    1.20  
    1.21 @@ -111,7 +111,6 @@
    1.22    | Space => "white space"
    1.23    | Comment => "comment text"
    1.24    | InternalValue => "internal value"
    1.25 -  | Malformed => "malformed symbolic character"
    1.26    | Error _ => "bad input"
    1.27    | Sync => "sync marker"
    1.28    | EOF => "end-of-file";
    1.29 @@ -331,7 +330,6 @@
    1.30      scan_verbatim >> token_range Verbatim ||
    1.31      scan_comment >> token_range Comment ||
    1.32      scan_space >> token Space ||
    1.33 -    Scan.one (Symbol.is_malformed o Symbol_Pos.symbol) >> (token Malformed o single) ||
    1.34      Scan.one (Symbol.is_sync o Symbol_Pos.symbol) >> (token Sync o single) ||
    1.35      (Scan.max token_leq
    1.36        (Scan.max token_leq