src/Pure/Isar/token.ML

 signature TOKEN =
 sig
   datatype kind =
     Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
     Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
-    Malformed | Error of string | Sync | EOF
+    Error of string | Sync | EOF
   datatype value =
     Text of string | Typ of typ | Term of term | Fact of thm list |
     Attribute of morphism -> attribute
   type T
   val str_of_kind: kind -> string

 (* datatype token *)
 
 datatype kind =
   Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
   Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
-  Malformed | Error of string | Sync | EOF;
+  Error of string | Sync | EOF;
 
 datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot;
 
 val str_of_kind =
  fn Command => "command"

   | AltString => "back-quoted string"
   | Verbatim => "verbatim text"
   | Space => "white space"
   | Comment => "comment text"
   | InternalValue => "internal value"
-  | Malformed => "malformed symbolic character"
   | Error _ => "bad input"
   | Sync => "sync marker"
   | EOF => "end-of-file";
 
 

   (Symbol_Pos.scan_string >> token_range String ||
     Symbol_Pos.scan_alt_string >> token_range AltString ||
     scan_verbatim >> token_range Verbatim ||
     scan_comment >> token_range Comment ||
     scan_space >> token Space ||
-    Scan.one (Symbol.is_malformed o Symbol_Pos.symbol) >> (token Malformed o single) ||
     Scan.one (Symbol.is_sync o Symbol_Pos.symbol) >> (token Sync o single) ||
     (Scan.max token_leq
       (Scan.max token_leq
         (Scan.literal lex2 >> pair Command)
         (Scan.literal lex1 >> pair Keyword))