src/Pure/Isar/outer_parse.ML

   type token
   val group: string -> (token list -> 'a) -> token list -> 'a
   val !!! : (token list -> 'a) -> token list -> 'a
   val $$$ : string -> token list -> string * token list
   val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
+  val command: token list -> string * token list
   val keyword: token list -> string * token list
   val short_ident: token list -> string * token list
   val long_ident: token list -> string * token list
   val sym_ident: token list -> string * token list
   val term_var: token list -> string * token list

 
 fun kind k =
   group (OuterLex.str_of_kind k)
     (Scan.one (OuterLex.is_kind k) >> OuterLex.val_of);
 
+val command = kind OuterLex.Command;
 val keyword = kind OuterLex.Keyword;
 val short_ident = kind OuterLex.Ident;
 val long_ident = kind OuterLex.LongIdent;
 val sym_ident = kind OuterLex.SymIdent;
 val term_var = kind OuterLex.Var;

 val sync = kind OuterLex.Sync;
 val eof = kind OuterLex.EOF;
 
 fun $$$ x =
   group (OuterLex.str_of_kind OuterLex.Keyword ^ " " ^ quote x)
-    (Scan.one (OuterLex.is_kind OuterLex.Keyword andf (equal x o OuterLex.val_of))
-      >> OuterLex.val_of);
+    (Scan.one (OuterLex.keyword_with (equal x)) >> OuterLex.val_of);
 
 val nat = number >> (fst o Term.read_int o Symbol.explode);
 
 val not_eof = Scan.one OuterLex.not_eof;
 

 val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) [];
 
 
 (* arguments *)
 
-fun keyword_symid is_symid = Scan.one (OuterLex.keyword_pred is_symid) >> OuterLex.val_of;
+fun keyword_symid is_symid = Scan.one (OuterLex.keyword_with is_symid) >> OuterLex.val_of;
 
 fun atom_arg is_symid blk =
   group "argument"
     (position (short_ident || long_ident || sym_ident || term_var || text_var ||
         type_ident || type_var || number) >> Args.ident ||