src/Pure/ML/ml_context.ML

   val thm: xstring -> thm
   val thms: xstring -> thm list
   val exec: (unit -> unit) -> Context.generic -> Context.generic
   val check_antiquotation: Proof.context -> xstring * Position.T -> string
   type decl = Proof.context -> string * string
-  val add_antiquotation: binding -> (Args.src -> Proof.context -> decl * Proof.context) ->
+  val add_antiquotation: binding -> (Token.src -> Proof.context -> decl * Proof.context) ->
     theory -> theory
   val print_antiquotations: Proof.context -> unit
   val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
     Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
   val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit

 (* theory data *)
 
 type decl = Proof.context -> string * string;  (*final context -> ML env, ML body*)
 structure Antiquotations = Theory_Data
 (
-  type T = (Args.src -> Proof.context -> decl * Proof.context) Name_Space.table;
+  type T = (Token.src -> Proof.context -> decl * Proof.context) Name_Space.table;
   val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
   val extend = I;
   fun merge data : T = Name_Space.merge_tables data;
 );
 

   Pretty.big_list "ML antiquotations:"
     (map (Pretty.mark_str o #1) (Name_Space.markup_table ctxt (get_antiquotations ctxt)))
   |> Pretty.writeln;
 
 fun apply_antiquotation src ctxt =
-  let val (src', f) = Args.check_src ctxt (get_antiquotations ctxt) src
+  let val (src', f) = Token.check_src ctxt (get_antiquotations ctxt) src
   in f src' ctxt end;
 
 
 (* parsing and evaluation *)
 
 local
 
 val antiq =
   Parse.!!! (Parse.position Parse.xname -- Parse.args --| Scan.ahead Parse.eof)
-  >> uncurry Args.src;
+  >> uncurry Token.src;
 
 val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
 
 fun begin_env visible =
   ML_Lex.tokenize