eliminated type Args.T;
pervasive types 'a parser and 'a context_parser;

--- a/src/Provers/blast.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Provers/blast.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -56,7 +56,7 @@
                  uwrappers: (string * wrapper) list,
                  safe0_netpair: netpair, safep_netpair: netpair,
                  haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
-  val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
+  val cla_modifiers: Method.modifier parser list
   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
   end;
 

--- a/src/Provers/clasimp.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Provers/clasimp.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -62,8 +62,8 @@
   val iff_add: attribute
   val iff_add': attribute
   val iff_del: attribute
-  val iff_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
-  val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
+  val iff_modifiers: Method.modifier parser list
+  val clasimp_modifiers: Method.modifier parser list
   val clasimp_setup: theory -> theory
 end;
 

--- a/src/Provers/classical.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Provers/classical.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -146,7 +146,7 @@
   val haz_elim: int option -> attribute
   val haz_intro: int option -> attribute
   val rule_del: attribute
-  val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
+  val cla_modifiers: Method.modifier parser list
   val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
   val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method

--- a/src/Provers/splitter.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Provers/splitter.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -39,7 +39,7 @@
   val Delsplits       : thm list -> unit
   val split_add: attribute
   val split_del: attribute
-  val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list
+  val split_modifiers : Method.modifier parser list
   val setup: theory -> theory
 end;
 

--- a/src/Pure/Isar/args.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Pure/Isar/args.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -7,69 +7,66 @@
 
 signature ARGS =
 sig
-  type T = OuterLex.token
+  type token = OuterLex.token
   type src
-  val src: (string * T list) * Position.T -> src
-  val dest_src: src -> (string * T list) * Position.T
+  val src: (string * token list) * Position.T -> src
+  val dest_src: src -> (string * token list) * Position.T
   val pretty_src: Proof.context -> src -> Pretty.T
   val map_name: (string -> string) -> src -> src
   val morph_values: morphism -> src -> src
   val maxidx_values: src -> int -> int
   val assignable: src -> src
   val closure: src -> src
-  val context: Context.generic * T list -> Context.proof * (Context.generic * T list)
-  val theory: Context.generic * T list -> Context.theory * (Context.generic * T list)
-  val $$$ : string -> T list -> string * T list
-  val add: T list -> string * T list
-  val del: T list -> string * T list
-  val colon: T list -> string * T list
-  val query: T list -> string * T list
-  val bang: T list -> string * T list
-  val query_colon: T list -> string * T list
-  val bang_colon: T list -> string * T list
-  val parens: (T list -> 'a * T list) -> T list -> 'a * T list
-  val bracks: (T list -> 'a * T list) -> T list -> 'a * T list
-  val mode: string -> 'a * T list -> bool * ('a * T list)
-  val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list
-  val name_source: T list -> string * T list
-  val name_source_position: T list -> (SymbolPos.text * Position.T) * T list
-  val name: T list -> string * T list
-  val binding: T list -> binding * T list
-  val alt_name: T list -> string * T list
-  val symbol: T list -> string * T list
-  val liberal_name: T list -> string * T list
-  val var: T list -> indexname * T list
-  val internal_text: T list -> string * T list
-  val internal_typ: T list -> typ * T list
-  val internal_term: T list -> term * T list
-  val internal_fact: T list -> thm list * T list
-  val internal_attribute: T list -> (morphism -> attribute) * T list
-  val named_text: (string -> string) -> T list -> string * T list
-  val named_typ: (string -> typ) -> T list -> typ * T list
-  val named_term: (string -> term) -> T list -> term * T list
-  val named_fact: (string -> thm list) -> T list -> thm list * T list
-  val named_attribute: (string -> morphism -> attribute) -> T list ->
-    (morphism -> attribute) * T list
-  val typ_abbrev: Context.generic * T list -> typ * (Context.generic * T list)
-  val typ: Context.generic * T list -> typ * (Context.generic * T list)
-  val term: Context.generic * T list -> term * (Context.generic * T list)
-  val term_abbrev: Context.generic * T list -> term * (Context.generic * T list)
-  val prop: Context.generic * T list -> term * (Context.generic * T list)
-  val tyname: Context.generic * T list -> string * (Context.generic * T list)
-  val const: Context.generic * T list -> string * (Context.generic * T list)
-  val const_proper: Context.generic * T list -> string * (Context.generic * T list)
-  val bang_facts: Context.generic * T list -> thm list * (Context.generic * T list)
-  val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
-    -> ((int -> tactic) -> tactic) * ('a * T list)
-  val parse: OuterLex.token list -> T list * OuterLex.token list
-  val parse1: (string -> bool) -> OuterLex.token list -> T list * OuterLex.token list
-  val attribs: (string -> string) -> T list -> src list * T list
-  val opt_attribs: (string -> string) -> T list -> src list * T list
-  val thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list
-  val opt_thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list
-  val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'a * 'b
-  val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
-    src -> Proof.context -> 'a * Proof.context
+  val context: Proof.context context_parser
+  val theory: theory context_parser
+  val $$$ : string -> string parser
+  val add: string parser
+  val del: string parser
+  val colon: string parser
+  val query: string parser
+  val bang: string parser
+  val query_colon: string parser
+  val bang_colon: string parser
+  val parens: ('a parser) -> 'a parser
+  val bracks: ('a parser) -> 'a parser
+  val mode: string -> bool context_parser
+  val maybe: 'a parser -> 'a option parser
+  val name_source: string parser
+  val name_source_position: (SymbolPos.text * Position.T) parser
+  val name: string parser
+  val binding: binding parser
+  val alt_name: string parser
+  val symbol: string parser
+  val liberal_name: string parser
+  val var: indexname parser
+  val internal_text: string parser
+  val internal_typ: typ parser
+  val internal_term: term parser
+  val internal_fact: thm list parser
+  val internal_attribute: (morphism -> attribute) parser
+  val named_text: (string -> string) -> string parser
+  val named_typ: (string -> typ) -> typ parser
+  val named_term: (string -> term) -> term parser
+  val named_fact: (string -> thm list) -> thm list parser
+  val named_attribute: (string -> morphism -> attribute) -> (morphism -> attribute) parser
+  val typ_abbrev: typ context_parser
+  val typ: typ context_parser
+  val term: term context_parser
+  val term_abbrev: term context_parser
+  val prop: term context_parser
+  val tyname: string context_parser
+  val const: string context_parser
+  val const_proper: string context_parser
+  val bang_facts: thm list context_parser
+  val goal_spec: ((int -> tactic) -> tactic) -> ((int -> tactic) -> tactic) context_parser
+  val parse: token list parser
+  val parse1: (string -> bool) -> token list parser
+  val attribs: (string -> string) -> src list parser
+  val opt_attribs: (string -> string) -> src list parser
+  val thm_name: (string -> string) -> string -> (binding * src list) parser
+  val opt_thm_name: (string -> string) -> string -> (binding * src list) parser
+  val syntax: string -> 'a context_parser -> src -> Context.generic -> 'a * Context.generic
+  val context_syntax: string -> 'a context_parser -> src -> Proof.context -> 'a * Proof.context
 end;
 
 structure Args: ARGS =
@@ -78,13 +75,13 @@
 structure T = OuterLex;
 structure P = OuterParse;
 
+type token = T.token;
+
 
 
 (** datatype src **)
 
-type T = T.token;
-
-datatype src = Src of (string * T list) * Position.T;
+datatype src = Src of (string * token list) * Position.T;
 
 val src = Src;
 fun dest_src (Src src) = src;

--- a/src/Pure/Isar/attrib.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -24,14 +24,13 @@
     (('c * 'att list) * ('d * 'att list) list) list
   val crude_closure: Proof.context -> src -> src
   val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
-  val syntax: (Context.generic * Args.T list ->
-    attribute * (Context.generic * Args.T list)) -> src -> attribute
+  val syntax: attribute context_parser -> src -> attribute
   val no_args: attribute -> src -> attribute
   val add_del_args: attribute -> attribute -> src -> attribute
-  val thm_sel: Args.T list -> Facts.interval list * Args.T list
-  val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list)
-  val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
-  val multi_thm: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
+  val thm_sel: Facts.interval list parser
+  val thm: thm context_parser
+  val thms: thm list context_parser
+  val multi_thm: thm list context_parser
   val print_configs: Proof.context -> unit
   val internal: (morphism -> attribute) -> src
   val register_config: Config.value Config.T -> theory -> theory

--- a/src/Pure/Isar/code.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Pure/Isar/code.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -44,7 +44,7 @@
   val postprocess_conv: theory -> cterm -> thm
   val postprocess_term: theory -> term -> term
 
-  val add_attribute: string * (Args.T list -> attribute * Args.T list) -> theory -> theory
+  val add_attribute: string * attribute parser -> theory -> theory
 
   val print_codesetup: theory -> unit
 end;
@@ -83,7 +83,7 @@
 (** code attributes **)
 
 structure CodeAttr = TheoryDataFun (
-  type T = (string * (Args.T list -> attribute * Args.T list)) list;
+  type T = (string * attribute parser) list;
   val empty = [];
   val copy = I;
   val extend = I;

--- a/src/Pure/Isar/outer_syntax.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -9,7 +9,6 @@
 
 signature OUTER_SYNTAX =
 sig
-  type 'a parser = 'a OuterParse.parser
   val command: string -> string -> OuterKeyword.T ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
   val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T ->

--- a/src/Pure/Isar/spec_parse.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Pure/Isar/spec_parse.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -6,8 +6,6 @@
 
 signature SPEC_PARSE =
 sig
-  type token = OuterParse.token
-  type 'a parser = 'a OuterParse.parser
   val attrib: Attrib.src parser
   val attribs: Attrib.src list parser
   val opt_attribs: Attrib.src list parser
@@ -36,8 +34,6 @@
 struct
 
 structure P = OuterParse;
-type token = P.token;
-type 'a parser = 'a P.parser;
 
 
 (* theorem specifications *)

--- a/src/Pure/Isar/value_parse.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Pure/Isar/value_parse.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -6,7 +6,6 @@
 
 signature VALUE_PARSE =
 sig
-  type 'a parser = 'a OuterParse.parser
   val comma: 'a parser -> 'a parser
   val equal: 'a parser -> 'a parser
   val parens: 'a parser -> 'a parser
@@ -20,7 +19,6 @@
 struct
 
 structure P = OuterParse;
-type 'a parser = 'a P.parser;
 
 
 (* syntax utilities *)

--- a/src/Pure/ML/ml_antiquote.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -6,15 +6,11 @@
 
 signature ML_ANTIQUOTE =
 sig
-  val macro: string ->
-    (Context.generic * Args.T list -> Proof.context * (Context.generic * Args.T list)) -> unit
+  val macro: string -> Proof.context context_parser -> unit
   val variant: string -> Proof.context -> string * Proof.context
-  val inline: string ->
-    (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
-  val declaration: string -> string ->
-    (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
-  val value: string ->
-    (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
+  val inline: string -> string context_parser -> unit
+  val declaration: string -> string -> string context_parser -> unit
+  val value: string -> string context_parser -> unit
 end;
 
 structure ML_Antiquote: ML_ANTIQUOTE =

--- a/src/Pure/ML/ml_context.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Pure/ML/ml_context.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -27,8 +27,7 @@
   type antiq =
     {struct_name: string, background: Proof.context} ->
       (Proof.context -> string * string) * Proof.context
-  val add_antiq: string ->
-    (Position.T -> Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) -> unit
+  val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
   val trace: bool ref
   val eval_wrapper: (string -> unit) * (string -> 'a) -> bool -> Position.T -> string -> unit
   val eval: bool -> Position.T -> string -> unit
@@ -157,9 +156,7 @@
 
 local
 
-val global_parsers = ref (Symtab.empty:
-  (Position.T -> Context.generic * Args.T list -> antiq * (Context.generic * Args.T list))
-    Symtab.table);
+val global_parsers = ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
 
 in
 

--- a/src/Pure/Thy/thy_output.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -18,8 +18,7 @@
   val print_antiquotations: unit -> unit
   val boolean: string -> bool
   val integer: string -> int
-  val antiquotation: string ->
-    (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
+  val antiquotation: string -> 'a context_parser ->
     ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
   datatype markup = Markup | MarkupEnv | Verbatim
   val modes: string list ref

--- a/src/Pure/simplifier.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Pure/simplifier.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -73,11 +73,10 @@
   val def_simproc_i: {name: string, lhss: term list,
     proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
     local_theory -> local_theory
-  val cong_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
-  val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
-  val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
-  val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
-    -> theory -> theory
+  val cong_modifiers: Method.modifier parser list
+  val simp_modifiers': Method.modifier parser list
+  val simp_modifiers: Method.modifier parser list
+  val method_setup: Method.modifier parser list -> theory -> theory
   val easy_setup: thm -> thm list -> theory -> theory
 end;
 

--- a/src/Tools/code/code_target.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Tools/code/code_target.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -26,7 +26,7 @@
     -> (Path.T option -> 'a -> unit)
     -> ('a -> string * string option list)
     -> 'a -> serialization
-  val serialize: theory -> string -> string option -> Args.T list
+  val serialize: theory -> string -> string option -> OuterLex.token list
     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
   val serialize_custom: theory -> string * (serializer * literals)
     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
@@ -106,7 +106,7 @@
 
 type serializer =
   string option                         (*module name*)
-  -> Args.T list                        (*arguments*)
+  -> OuterLex.token list                (*arguments*)
   -> (string -> string)                 (*labelled_name*)
   -> string list                        (*reserved symbols*)
   -> (string * Pretty.T) list           (*includes*)

--- a/src/Tools/eqsubst.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Tools/eqsubst.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -109,8 +109,8 @@
        searchinfo -> Term.term -> match Seq.seq Seq.seq
 
     (* syntax tools *)
-    val ith_syntax : Args.T list -> int list * Args.T list
-    val options_syntax : Args.T list -> bool * Args.T list
+    val ith_syntax : int list parser
+    val options_syntax : bool parser
 
     (* Isar level hooks *)
     val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method