src/Pure/Syntax/lexicon.ML

   val scan_var: Symbol_Pos.T list scanner
   val scan_tvar: Symbol_Pos.T list scanner
   val is_tid: string -> bool
   datatype token_kind =
     Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str |
-    String | Cartouche | Space | Comment of Comment.kind option | Dummy | EOF
+    String | Cartouche | Space | Comment of Comment.kind | Dummy | EOF
   eqtype token
   val kind_of_token: token -> token_kind
   val str_of_token: token -> string
   val pos_of_token: token -> Position.T
   val end_pos_of_token: token -> Position.T

 
 (* datatype token_kind *)
 
 datatype token_kind =
   Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str |
-  String | Cartouche | Space | Comment of Comment.kind option | Dummy | EOF;
+  String | Cartouche | Space | Comment of Comment.kind | Dummy | EOF;
 
 val token_kinds =
   Vector.fromList
    [Literal, Ident, Long_Ident, Var, Type_Ident, Type_Var, Num, Float, Str,
-    String, Cartouche, Space, Comment NONE, Comment (SOME Comment.Comment),
-    Comment (SOME Comment.Cancel), Comment (SOME Comment.Latex), Dummy, EOF];
+    String, Cartouche, Space, Comment Comment.Comment, Comment Comment.Cancel,
+    Comment Comment.Latex, Dummy, EOF];
 
 fun token_kind i = Vector.sub (token_kinds, i);
 fun token_kind_index k = #1 (the (Vector.findi (fn (_, k') => k = k') token_kinds));
 
 

 
     val scan_lit = Scan.literal lex >> token Literal;
 
     val scan =
       Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
-      Symbol_Pos.scan_comment err_prefix >> token (Comment NONE) ||
-      Comment.scan >> (fn (kind, ss) => token (Comment (SOME kind)) ss) ||
+      Comment.scan >> (fn (kind, ss) => token (Comment kind) ss) ||
       Scan.max token_leq scan_lit scan_val ||
       scan_string >> token String ||
       scan_str >> token Str ||
       Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space;
   in