src/Pure/Isar/outer_lex.ML

   keep_line (Scan.one Symbol.is_blank);
 
 
 (* scan symbolic idents *)
 
-val sym_chars = explode "!#$%&*+-/:<=>?@^_|~";
+val sym_chars = explode "!#$%&*+-/<=>?@^_|~";
 fun is_sym_char s = s mem sym_chars;
 
 val scan_symid =
   Scan.any1 is_sym_char >> implode ||
   Scan.one Symbol.is_symbolic;

   (case try Symbol.explode str of
     SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
   | SOME ss => forall is_sym_char ss
   | _ => false);
 
-val is_sid = is_symid orf Syntax.is_identifier;
+fun is_sid s = s = ":" orelse is_symid s orelse Syntax.is_identifier s;
 
 
 (* scan strings *)
 
 local