src/Pure/Isar/outer_parse.ML

   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
-  val text_var: token list -> string * token list
   val type_ident: token list -> string * token list
   val type_var: token list -> string * token list
   val number: token list -> string * token list
   val string: token list -> string * token list
   val verbatim: token list -> string * token list

 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 text_var = kind OuterLex.TextVar;
 val type_ident = kind OuterLex.TypeIdent;
 val type_var = kind OuterLex.TypeVar;
 val number = kind OuterLex.Nat;
 val string = kind OuterLex.String;
 val verbatim = kind OuterLex.Verbatim;

   name -- ($$$ "::" |-- !!! (typ -- opt_mixfix)) >> triple2;
 
 
 (* terms *)
 
-val trm = short_ident || long_ident || sym_ident || term_var || text_var || number || string;
+val trm = short_ident || long_ident || sym_ident || term_var || number || string;
 
 val term = group "term" trm;
 val prop = group "proposition" trm;
 
 

 
 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 ||
+    (position (short_ident || long_ident || sym_ident || term_var ||
         type_ident || type_var || number) >> Args.ident ||
       position (keyword_symid is_symid) >> Args.keyword ||
       position string >> Args.string ||
       position (if blk then $$$ "," else Scan.fail) >> Args.keyword);