# HG changeset patch
# User wenzelm
# Date 1408483071 -7200
# Node ID bc6bced136e5dd0c29e4e2132996214af7b96ae1
# Parent  568840962230b1a3a5de7b1c2dcab9f26653317e
tuned signature -- moved type src to Token, without aliases;

diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -21,17 +21,17 @@
   val nesting_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
 
   type lfp_sugar_thms =
-    (thm list * thm * Args.src list) * (thm list list * Args.src list)
+    (thm list * thm * Token.src list) * (thm list list * Token.src list)
 
   val morph_lfp_sugar_thms: morphism -> lfp_sugar_thms -> lfp_sugar_thms
   val transfer_lfp_sugar_thms: Proof.context -> lfp_sugar_thms -> lfp_sugar_thms
 
   type gfp_sugar_thms =
-    ((thm list * thm) list * (Args.src list * Args.src list))
+    ((thm list * thm) list * (Token.src list * Token.src list))
     * thm list list
     * thm list list
-    * (thm list list * Args.src list)
-    * (thm list list list * Args.src list)
+    * (thm list list * Token.src list)
+    * (thm list list list * Token.src list)
 
   val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms
   val transfer_gfp_sugar_thms: Proof.context -> gfp_sugar_thms -> gfp_sugar_thms
@@ -304,7 +304,7 @@
 fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p;
 
 type lfp_sugar_thms =
-  (thm list * thm * Args.src list) * (thm list list * Args.src list);
+  (thm list * thm * Token.src list) * (thm list list * Token.src list);
 
 fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (recss, rec_attrs)) =
   ((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs),
@@ -315,11 +315,11 @@
   morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
 
 type gfp_sugar_thms =
-  ((thm list * thm) list * (Args.src list * Args.src list))
+  ((thm list * thm) list * (Token.src list * Token.src list))
   * thm list list
   * thm list list
-  * (thm list list * Args.src list)
-  * (thm list list list * Args.src list);
+  * (thm list list * Token.src list)
+  * (thm list list list * Token.src list);
 
 fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs_pair),
     corecss, corec_discss, (corec_disc_iffss, corec_disc_iff_attrs),
diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -12,7 +12,7 @@
   defname : string,
     (* contains no logical entities: invariant under morphisms: *)
   add_simps : (binding -> binding) -> string -> (binding -> binding) ->
-    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+    Token.src list -> thm list -> local_theory -> thm list * local_theory,
   fnames : string list,
   case_names : string list,
   fs : term list,
@@ -37,7 +37,7 @@
   defname : string,
     (* contains no logical entities: invariant under morphisms: *)
   add_simps : (binding -> binding) -> string -> (binding -> binding) ->
-    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+    Token.src list -> thm list -> local_theory -> thm list * local_theory,
   fnames : string list,
   case_names : string list,
   fs : term list,
diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -13,7 +13,8 @@
     (binding * mixfix) -> typ -> term -> thm -> thm list -> local_theory -> local_theory
 
   val lift_def_cmd:
-    (binding * string option * mixfix) * string * (Facts.ref * Args.src list) list -> local_theory -> Proof.state
+    (binding * string option * mixfix) * string * (Facts.ref * Token.src list) list ->
+    local_theory -> Proof.state
 
   val can_generate_code_cert: thm -> bool
 end
diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -223,7 +223,7 @@
     val dummy_thm = Thm.transfer thy Drule.dummy_thm
     val pointer = Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none bundle_name
     val restore_lifting_att = 
-      ([dummy_thm], [Args.src ("Lifting.lifting_restore_internal", Position.none) pointer])
+      ([dummy_thm], [Token.src ("Lifting.lifting_restore_internal", Position.none) pointer])
   in
     lthy 
       |> Local_Theory.declaration {syntax = false, pervasive = true}
@@ -969,7 +969,7 @@
     case bundle of
       [(_, [arg_src])] => 
         let
-          val (name, _) = Args.syntax (Scan.lift Args.name) arg_src ctxt
+          val (name, _) = Token.syntax (Scan.lift Args.name) arg_src ctxt
             handle ERROR _ => error "The provided bundle is not a lifting bundle."
         in name end
       | _ => error "The provided bundle is not a lifting bundle."
diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -13,7 +13,7 @@
     ((binding * binding) option * bool * thm option) -> Proof.context -> Proof.state
 
   val quotient_type_cmd: ((((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
-    (binding * binding) option) * (Facts.ref * Args.src list) option -> Proof.context -> Proof.state
+    (binding * binding) option) * (Facts.ref * Token.src list) option -> Proof.context -> Proof.state
 end;
 
 structure Quotient_Type: QUOTIENT_TYPE =
diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -14,15 +14,15 @@
   type fact = (string * stature) * thm
 
   type fact_override =
-    {add : (Facts.ref * Attrib.src list) list,
-     del : (Facts.ref * Attrib.src list) list,
+    {add : (Facts.ref * Token.src list) list,
+     del : (Facts.ref * Token.src list) list,
      only : bool}
 
   val instantiate_inducts : bool Config.T
   val no_fact_override : fact_override
 
   val fact_of_ref : Proof.context -> unit Symtab.table -> thm list -> status Termtab.table ->
-    Facts.ref * Attrib.src list -> ((string * stature) * thm) list
+    Facts.ref * Token.src list -> ((string * stature) * thm) list
   val backquote_thm : Proof.context -> thm -> string
   val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
   val clasimpset_rule_table_of : Proof.context -> status Termtab.table
@@ -50,8 +50,8 @@
 type fact = (string * stature) * thm
 
 type fact_override =
-  {add : (Facts.ref * Attrib.src list) list,
-   del : (Facts.ref * Attrib.src list) list,
+  {add : (Facts.ref * Token.src list) list,
+   del : (Facts.ref * Token.src list) list,
    only : bool}
 
 (* gracefully handle huge background theories *)
@@ -159,7 +159,7 @@
 fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) =
   let
     val ths = Attrib.eval_thms ctxt [xthm]
-    val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args)
+    val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src ctxt) args)
 
     fun nth_name j =
       (case xref of
diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/inductive.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -53,7 +53,7 @@
     (binding * string option * mixfix) list ->
     (binding * string option * mixfix) list ->
     (Attrib.binding * string) list ->
-    (Facts.ref * Attrib.src list) list ->
+    (Facts.ref * Token.src list) list ->
     local_theory -> inductive_result * local_theory
   val add_inductive_global: inductive_flags ->
     ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
@@ -76,7 +76,7 @@
     term list -> (binding * mixfix) list ->
     local_theory -> inductive_result * local_theory
   val declare_rules: binding -> bool -> bool -> string list -> term list ->
-    thm list -> binding list -> Attrib.src list list -> (thm * string list * int) list ->
+    thm list -> binding list -> Token.src list list -> (thm * string list * int) list ->
     thm list -> thm -> local_theory -> thm list * thm list * thm list * thm * thm list * local_theory
   val add_ind_def: add_ind_def
   val gen_add_inductive_i: add_ind_def -> inductive_flags ->
@@ -85,7 +85,7 @@
   val gen_add_inductive: add_ind_def -> bool -> bool ->
     (binding * string option * mixfix) list ->
     (binding * string option * mixfix) list ->
-    (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
+    (Attrib.binding * string) list -> (Facts.ref * Token.src list) list ->
     local_theory -> inductive_result * local_theory
   val gen_ind_decl: add_ind_def -> bool -> (local_theory -> local_theory) parser
 end;
diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -20,7 +20,7 @@
   val add_inductive: bool -> bool ->
     (binding * string option * mixfix) list ->
     (binding * string option * mixfix) list ->
-    (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
+    (Attrib.binding * string) list -> (Facts.ref * Token.src list) list ->
     local_theory -> Inductive.inductive_result * local_theory
   val mono_add: attribute
   val mono_del: attribute
diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/recdef.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -15,17 +15,17 @@
   val cong_del: attribute
   val wf_add: attribute
   val wf_del: attribute
-  val add_recdef: bool -> xstring -> string -> ((binding * string) * Attrib.src list) list ->
-    Attrib.src option -> theory -> theory
+  val add_recdef: bool -> xstring -> string -> ((binding * string) * Token.src list) list ->
+    Token.src option -> theory -> theory
       * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
     theory -> theory * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
-  val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list
+  val defer_recdef: xstring -> string list -> (Facts.ref * Token.src list) list
     -> theory -> theory * {induct_rules: thm}
   val defer_recdef_i: xstring -> term list -> thm list -> theory -> theory * {induct_rules: thm}
-  val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> bool ->
+  val recdef_tc: bstring * Token.src list -> xstring -> int option -> bool ->
     local_theory -> Proof.state
-  val recdef_tc_i: bstring * Attrib.src list -> string -> int option -> bool ->
+  val recdef_tc_i: bstring * Token.src list -> string -> int option -> bool ->
     local_theory -> Proof.state
   val setup: theory -> theory
 end;
@@ -164,7 +164,7 @@
     val ctxt =
       (case opt_src of
         NONE => ctxt0
-      | SOME src => #2 (Args.syntax (Method.sections recdef_modifiers) src ctxt0));
+      | SOME src => #2 (Token.syntax (Method.sections recdef_modifiers) src ctxt0));
     val {simps, congs, wfs} = get_hints ctxt;
     val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong};
   in (ctxt', rev (map snd congs), wfs) end;
@@ -292,7 +292,7 @@
 val hints =
   @{keyword "("} |--
     Parse.!!! (Parse.position @{keyword "hints"} -- Parse.args --| @{keyword ")"})
-  >> uncurry Args.src;
+  >> uncurry Token.src;
 
 val recdef_decl =
   Scan.optional
diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/try0.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -173,7 +173,7 @@
 
 fun string_of_xthm (xref, args) =
   Facts.string_of_ref xref ^
-  implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src @{context}) args);
+  implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src @{context}) args);
 
 val parse_fact_refs =
   Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse_Spec.xthm >> string_of_xthm));
diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/args.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -1,22 +1,12 @@
 (*  Title:      Pure/Isar/args.ML
     Author:     Markus Wenzel, TU Muenchen
 
-Parsing with implicit value assignment.  Concrete argument syntax of
+Quasi-inner syntax based on outer tokens: concrete argument syntax of
 attributes, methods etc.
 *)
 
 signature ARGS =
 sig
-  type src
-  val src: xstring * Position.T -> Token.T list -> src
-  val name_of_src: src -> string * Position.T
-  val range_of_src: src -> Position.T
-  val unparse_src: src -> string list
-  val pretty_src: Proof.context -> src -> Pretty.T
-  val check_src: Proof.context -> 'a Name_Space.table -> src -> src * 'a
-  val transform_values: morphism -> src -> src
-  val init_assignable: src -> src
-  val closure: src -> src
   val context: Proof.context context_parser
   val theory: theory context_parser
   val $$$ : string -> string parser
@@ -62,67 +52,13 @@
   val type_name: {proper: bool, strict: bool} -> string context_parser
   val const: {proper: bool, strict: bool} -> string context_parser
   val goal_spec: ((int -> tactic) -> tactic) context_parser
-  val attribs: (xstring * Position.T -> string) -> src list parser
-  val opt_attribs: (xstring * Position.T -> string) -> src list parser
-  val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
-  val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
+  val attribs: (xstring * Position.T -> string) -> Token.src list parser
+  val opt_attribs: (xstring * Position.T -> string) -> Token.src list parser
 end;
 
 structure Args: ARGS =
 struct
 
-(** datatype src **)
-
-datatype src =
-  Src of
-   {name: string * Position.T,
-    args: Token.T list,
-    output_info: (string * Markup.T) option};
-
-fun src name args = Src {name = name, args = args, output_info = NONE};
-
-fun name_of_src (Src {name, ...}) = name;
-
-fun range_of_src (Src {name = (_, pos), args, ...}) =
-  if null args then pos
-  else Position.set_range (pos, #2 (Token.range_of args));
-
-fun unparse_src (Src {args, ...}) = map Token.unparse args;
-
-fun pretty_src ctxt src =
-  let
-    val Src {name = (name, _), args, output_info} = src;
-    val prt_name =
-      (case output_info of
-        NONE => Pretty.str name
-      | SOME (_, markup) => Pretty.mark_str (markup, name));
-    val prt_arg = Token.pretty_value ctxt;
-  in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
-
-
-(* check *)
-
-fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) =
-  let
-    val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
-    val space = Name_Space.space_of_table table;
-    val kind = Name_Space.kind_of space;
-    val markup = Name_Space.markup space name;
-  in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end;
-
-
-(* values *)
-
-fun map_args f (Src {name, args, output_info}) =
-  Src {name = name, args = map f args, output_info = output_info};
-
-val transform_values = map_args o Token.transform_value;
-
-val init_assignable = map_args Token.init_assignable;
-val closure = map_args Token.closure;
-
-
-
 (** argument scanners **)
 
 (* context *)
@@ -251,42 +187,9 @@
   let
     fun intern tok = check (Token.content_of tok, Token.pos_of tok);
     val attrib_name = internal_name >> #1 || (symbolic || named) >> evaluate Token.name0 intern;
-    val attrib = Parse.position attrib_name -- Parse.!!! Parse.args >> uncurry src;
+    val attrib = Parse.position attrib_name -- Parse.!!! Parse.args >> uncurry Token.src;
   in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
 
 fun opt_attribs check = Scan.optional (attribs check) [];
 
-
-
-(** syntax wrapper **)
-
-fun syntax_generic scan (Src {name = (name, pos), args = args0, output_info}) context =
-  let
-    val args1 = map Token.init_assignable args0;
-    fun reported_text () =
-      if Context_Position.is_visible_generic context then
-        ((pos, Markup.operator) :: maps (Token.reports_of_value o Token.closure) args1)
-        |> map (fn (p, m) => Position.reported_text p m "")
-      else [];
-  in
-    (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (context, args1) of
-      (SOME x, (context', [])) =>
-        let val _ = Output.report (reported_text ())
-        in (x, context') end
-    | (_, (_, args2)) =>
-        let
-          val print_name =
-            (case output_info of
-              NONE => quote name
-            | SOME (kind, markup) => plain_words kind ^ " " ^ quote (Markup.markup markup name));
-          val print_args =
-            if null args2 then "" else ":\n  " ^ space_implode " " (map Token.print args2);
-        in
-          error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^
-            Markup.markup_report (implode (reported_text ())))
-        end)
-  end;
-
-fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof;
-
 end;
diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -6,23 +6,22 @@
 
 signature ATTRIB =
 sig
-  type src = Args.src
-  type binding = binding * src list
+  type binding = binding * Token.src list
   val empty_binding: binding
   val is_empty_binding: binding -> bool
   val print_attributes: Proof.context -> unit
-  val define_global: Binding.binding -> (Args.src -> attribute) ->
+  val define_global: Binding.binding -> (Token.src -> attribute) ->
     string -> theory -> string * theory
-  val define: Binding.binding -> (Args.src -> attribute) ->
+  val define: Binding.binding -> (Token.src -> attribute) ->
     string -> local_theory -> string * local_theory
   val check_name_generic: Context.generic -> xstring * Position.T -> string
   val check_name: Proof.context -> xstring * Position.T -> string
-  val check_src: Proof.context -> src -> src
-  val pretty_attribs: Proof.context -> src list -> Pretty.T list
-  val attribute: Proof.context -> src -> attribute
-  val attribute_global: theory -> src -> attribute
-  val attribute_cmd: Proof.context -> src -> attribute
-  val attribute_cmd_global: theory -> src -> attribute
+  val check_src: Proof.context -> Token.src -> Token.src
+  val pretty_attribs: Proof.context -> Token.src list -> Pretty.T list
+  val attribute: Proof.context -> Token.src -> attribute
+  val attribute_global: theory -> Token.src -> attribute
+  val attribute_cmd: Proof.context -> Token.src -> attribute
+  val attribute_cmd_global: theory -> Token.src -> attribute
   val map_specs: ('a list -> 'att list) ->
     (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
   val map_facts: ('a list -> 'att list) ->
@@ -31,28 +30,28 @@
   val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
     (('c * 'a list) * ('b * 'a list) list) list ->
     (('c * 'att list) * ('fact * 'att list) list) list
-  val global_notes: string -> (binding * (thm list * src list) list) list ->
+  val global_notes: string -> (binding * (thm list * Token.src list) list) list ->
     theory -> (string * thm list) list * theory
-  val local_notes: string -> (binding * (thm list * src list) list) list ->
+  val local_notes: string -> (binding * (thm list * Token.src list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
-  val generic_notes: string -> (binding * (thm list * src list) list) list ->
+  val generic_notes: string -> (binding * (thm list * Token.src list) list) list ->
     Context.generic -> (string * thm list) list * Context.generic
-  val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
-  val attribute_syntax: attribute context_parser -> Args.src -> attribute
+  val eval_thms: Proof.context -> (Facts.ref * Token.src list) list -> thm list
+  val attribute_syntax: attribute context_parser -> Token.src -> attribute
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
   val local_setup: Binding.binding -> attribute context_parser -> string ->
     local_theory -> local_theory
   val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
     local_theory -> local_theory
-  val internal: (morphism -> attribute) -> src
+  val internal: (morphism -> attribute) -> Token.src
   val add_del: attribute -> attribute -> attribute context_parser
   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 partial_evaluation: Proof.context ->
-    (binding * (thm list * Args.src list) list) list ->
-    (binding * (thm list * Args.src list) list) list
+    (binding * (thm list * Token.src list) list) list ->
+    (binding * (thm list * Token.src list) list) list
   val print_options: Proof.context -> unit
   val config_bool: Binding.binding ->
     (Context.generic -> bool) -> bool Config.T * (theory -> theory)
@@ -81,8 +80,7 @@
 
 (* source and bindings *)
 
-type src = Args.src;
-type binding = binding * src list;
+type binding = binding * Token.src list;
 
 val empty_binding: binding = (Binding.empty, []);
 fun is_empty_binding ((b, srcs): binding) = Binding.is_empty b andalso null srcs;
@@ -95,7 +93,7 @@
 
 structure Attributes = Generic_Data
 (
-  type T = ((src -> attribute) * string) Name_Space.table;
+  type T = ((Token.src -> attribute) * string) Name_Space.table;
   val empty : T = Name_Space.empty_table "attribute";
   val extend = I;
   fun merge data : T = Name_Space.merge_tables data;
@@ -147,21 +145,21 @@
 val check_name = check_name_generic o Context.Proof;
 
 fun check_src ctxt src =
- (Context_Position.report ctxt (Args.range_of_src src) Markup.language_attribute;
-  #1 (Args.check_src ctxt (get_attributes ctxt) src));
+ (Context_Position.report ctxt (Token.range_of_src src) Markup.language_attribute;
+  #1 (Token.check_src ctxt (get_attributes ctxt) src));
 
 
 (* pretty printing *)
 
 fun pretty_attribs _ [] = []
-  | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt) srcs)];
+  | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Token.pretty_src ctxt) srcs)];
 
 
 (* get attributes *)
 
 fun attribute_generic context =
   let val table = Attributes.get context
-  in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
+  in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end;
 
 val attribute = attribute_generic o Context.Proof;
 val attribute_global = attribute_generic o Context.Theory;
@@ -199,7 +197,7 @@
 (* attribute setup *)
 
 fun attribute_syntax scan src (context, th) =
-  let val (a, context') = Args.syntax_generic scan src context in a (context', th) end;
+  let val (a, context') = Token.syntax_generic scan src context in a (context', th) end;
 
 fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd;
 fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
@@ -216,7 +214,7 @@
 
 (* internal attribute *)
 
-fun internal att = Args.src ("Pure.attribute", Position.none) [Token.mk_attribute att];
+fun internal att = Token.src ("Pure.attribute", Position.none) [Token.mk_attribute att];
 
 val _ = Theory.setup
   (setup (Binding.make ("attribute", @{here}))
@@ -287,13 +285,13 @@
 
 fun apply_att src (context, th) =
   let
-    val src1 = Args.init_assignable src;
+    val src1 = Token.init_assignable_src src;
     val result = attribute_generic context src1 (context, th);
-    val src2 = Args.closure src1;
+    val src2 = Token.closure_src src1;
   in (src2, result) end;
 
 fun err msg src =
-  let val (name, pos) = Args.name_of_src src
+  let val (name, pos) = Token.name_of_src src
   in error (msg ^ " " ^ quote name ^ Position.here pos) end;
 
 fun eval src ((th, dyn), (decls, context)) =
diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/bundle.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -6,13 +6,13 @@
 
 signature BUNDLE =
 sig
-  type bundle = (thm list * Args.src list) list
+  type bundle = (thm list * Token.src list) list
   val check: Proof.context -> xstring * Position.T -> string
   val get_bundle: Proof.context -> string -> bundle
   val get_bundle_cmd: Proof.context -> xstring * Position.T -> bundle
-  val bundle: binding * (thm list * Args.src list) list ->
+  val bundle: binding * (thm list * Token.src list) list ->
     (binding * typ option * mixfix) list -> local_theory -> local_theory
-  val bundle_cmd: binding * (Facts.ref * Args.src list) list ->
+  val bundle_cmd: binding * (Facts.ref * Token.src list) list ->
     (binding * string option * mixfix) list -> local_theory -> local_theory
   val includes: string list -> Proof.context -> Proof.context
   val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
@@ -31,10 +31,10 @@
 
 (* maintain bundles *)
 
-type bundle = (thm list * Args.src list) list;
+type bundle = (thm list * Token.src list) list;
 
 fun transform_bundle phi : bundle -> bundle =
-  map (fn (fact, atts) => (Morphism.fact phi fact, map (Args.transform_values phi) atts));
+  map (fn (fact, atts) => (Morphism.fact phi fact, map (Token.transform_src phi) atts));
 
 structure Data = Generic_Data
 (
diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/calculation.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -14,10 +14,10 @@
   val sym_del: attribute
   val symmetric: attribute
   val also: thm list option -> bool -> Proof.state -> Proof.state Seq.result Seq.seq
-  val also_cmd: (Facts.ref * Attrib.src list) list option ->
+  val also_cmd: (Facts.ref * Token.src list) list option ->
     bool -> Proof.state -> Proof.state Seq.result Seq.seq
   val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.result Seq.seq
-  val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool ->
+  val finally_cmd: (Facts.ref * Token.src list) list option -> bool ->
     Proof.state -> Proof.state Seq.result Seq.seq
   val moreover: bool -> Proof.state -> Proof.state
   val ultimately: bool -> Proof.state -> Proof.state
diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/code.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -49,13 +49,13 @@
   val add_nbe_eqn: thm -> theory -> theory
   val add_abs_eqn: thm -> theory -> theory
   val add_abs_eqn_attribute: attribute
-  val add_abs_eqn_attrib: Attrib.src
+  val add_abs_eqn_attrib: Token.src
   val add_default_eqn: thm -> theory -> theory
   val add_default_eqn_attribute: attribute
-  val add_default_eqn_attrib: Attrib.src
+  val add_default_eqn_attrib: Token.src
   val add_nbe_default_eqn: thm -> theory -> theory
   val add_nbe_default_eqn_attribute: attribute
-  val add_nbe_default_eqn_attrib: Attrib.src
+  val add_nbe_default_eqn_attrib: Token.src
   val del_eqn: thm -> theory -> theory
   val del_eqns: string -> theory -> theory
   val del_exception: string -> theory -> theory
diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/element.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -17,18 +17,18 @@
     Constrains of (string * 'typ) list |
     Assumes of (Attrib.binding * ('term * 'term list) list) list |
     Defines of (Attrib.binding * ('term * 'term list)) list |
-    Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list
+    Notes of string * (Attrib.binding * ('fact * Token.src list) list) list
   type context = (string, string, Facts.ref) ctxt
   type context_i = (typ, term, thm list) ctxt
   val map_ctxt: {binding: binding -> binding, typ: 'typ -> 'a, term: 'term -> 'b,
-    pattern: 'term -> 'b, fact: 'fact -> 'c, attrib: Attrib.src -> Attrib.src} ->
+    pattern: 'term -> 'b, fact: 'fact -> 'c, attrib: Token.src -> Token.src} ->
     ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
-  val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
+  val map_ctxt_attrib: (Token.src -> Token.src) ->
     ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
   val transform_ctxt: morphism -> context_i -> context_i
   val transform_facts: morphism ->
-    (Attrib.binding * (thm list * Args.src list) list) list ->
-    (Attrib.binding * (thm list * Args.src list) list) list
+    (Attrib.binding * (thm list * Token.src list) list) list ->
+    (Attrib.binding * (thm list * Token.src list) list) list
   val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
   val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
   val pretty_statement: Proof.context -> string -> thm -> Pretty.T
@@ -78,7 +78,7 @@
   Constrains of (string * 'typ) list |
   Assumes of (Attrib.binding * ('term * 'term list) list) list |
   Defines of (Attrib.binding * ('term * 'term list)) list |
-  Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list;
+  Notes of string * (Attrib.binding * ('fact * Token.src list) list) list;
 
 type context = (string, string, Facts.ref) ctxt;
 type context_i = (typ, term, thm list) ctxt;
@@ -103,7 +103,7 @@
   term = Morphism.term phi,
   pattern = Morphism.term phi,
   fact = Morphism.fact phi,
-  attrib = Args.transform_values phi};
+  attrib = Token.transform_src phi};
 
 fun transform_facts phi facts =
   Notes ("", facts) |> transform_ctxt phi |> (fn Notes (_, facts') => facts');
@@ -509,14 +509,14 @@
 fun activate_i elem ctxt =
   let
     val elem' =
-      (case map_ctxt_attrib Args.init_assignable elem of
+      (case map_ctxt_attrib Token.init_assignable_src elem of
         Defines defs =>
           Defines (defs |> map (fn ((a, atts), (t, ps)) =>
             ((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt t)))) a, atts),
               (t, ps))))
       | e => e);
     val ctxt' = Context.proof_map (init elem') ctxt;
-  in (map_ctxt_attrib Args.closure elem', ctxt') end;
+  in (map_ctxt_attrib Token.closure_src elem', ctxt') end;
 
 fun activate raw_elem ctxt =
   let val elem = raw_elem |> map_ctxt
diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -23,9 +23,9 @@
     bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val notes:
-    (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
-      (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) ->
-    string -> (Attrib.binding * (thm list * Args.src list) list) list -> local_theory ->
+    (string -> (Attrib.binding * (thm list * Token.src list) list) list ->
+      (Attrib.binding * (thm list * Token.src list) list) list -> local_theory -> local_theory) ->
+    string -> (Attrib.binding * (thm list * Token.src list) list) list -> local_theory ->
     (string * thm list) list * local_theory
   val abbrev: (string * bool -> binding * mixfix -> term ->
       term list * term list -> local_theory -> local_theory) ->
@@ -35,8 +35,8 @@
   val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     term list * term list -> local_theory -> (term * thm) * local_theory
   val theory_notes: string ->
-    (Attrib.binding * (thm list * Args.src list) list) list ->
-    (Attrib.binding * (thm list * Args.src list) list) list ->
+    (Attrib.binding * (thm list * Token.src list) list) list ->
+    (Attrib.binding * (thm list * Token.src list) list) list ->
     local_theory -> local_theory
   val theory_declaration: declaration -> local_theory -> local_theory
   val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
@@ -46,8 +46,8 @@
 
   (* locale operations *)
   val locale_notes: string -> string ->
-    (Attrib.binding * (thm list * Args.src list) list) list ->
-    (Attrib.binding * (thm list * Args.src list) list) list ->
+    (Attrib.binding * (thm list * Token.src list) list) list ->
+    (Attrib.binding * (thm list * Token.src list) list) list ->
     local_theory -> local_theory
   val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
   val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration ->
diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -16,7 +16,7 @@
   val translations: (xstring * string) Syntax.trrule list -> theory -> theory
   val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
   val oracle: bstring * Position.T -> Symbol_Pos.source -> theory -> theory
-  val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
+  val add_defs: (bool * bool) * ((binding * string) * Token.src list) list -> theory -> theory
   val declaration: {syntax: bool, pervasive: bool} ->
     Symbol_Pos.source -> local_theory -> local_theory
   val simproc_setup: string * Position.T -> string list -> Symbol_Pos.source ->
@@ -39,11 +39,11 @@
   val thy_deps: Toplevel.transition -> Toplevel.transition
   val locale_deps: Toplevel.transition -> Toplevel.transition
   val class_deps: Toplevel.transition -> Toplevel.transition
-  val print_stmts: string list * (Facts.ref * Attrib.src list) list
+  val print_stmts: string list * (Facts.ref * Token.src list) list
     -> Toplevel.transition -> Toplevel.transition
-  val print_thms: string list * (Facts.ref * Attrib.src list) list
+  val print_thms: string list * (Facts.ref * Token.src list) list
     -> Toplevel.transition -> Toplevel.transition
-  val print_prfs: bool -> string list * (Facts.ref * Attrib.src list) list option
+  val print_prfs: bool -> string list * (Facts.ref * Token.src list) list option
     -> Toplevel.transition -> Toplevel.transition
   val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
   val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/local_theory.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -9,8 +9,7 @@
 
 structure Attrib =
 struct
-  type src = Args.src;
-  type binding = binding * src list;
+  type binding = binding * Token.src list;
 end;
 
 signature LOCAL_THEORY =
@@ -49,9 +48,9 @@
   val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
-  val notes: (Attrib.binding * (thm list * Attrib.src list) list) list ->
+  val notes: (Attrib.binding * (thm list * Token.src list) list) list ->
     local_theory -> (string * thm list) list * local_theory
-  val notes_kind: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
+  val notes_kind: string -> (Attrib.binding * (thm list * Token.src list) list) list ->
     local_theory -> (string * thm list) list * local_theory
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
@@ -87,7 +86,7 @@
  {define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory,
   notes: string ->
-    (Attrib.binding * (thm list * Attrib.src list) list) list ->
+    (Attrib.binding * (thm list * Token.src list) list) list ->
     local_theory -> (string * thm list) list * local_theory,
   abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory,
diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -34,7 +34,7 @@
     term option * term list ->
     thm option * thm option -> thm list ->
     declaration list ->
-    (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
+    (string * (Attrib.binding * (thm list * Token.src list) list) list) list ->
     (string * morphism) list -> theory -> theory
   val intern: theory -> xstring -> string
   val check: theory -> xstring * Position.T -> string
@@ -49,7 +49,7 @@
   val specification_of: theory -> string -> term option * term list
 
   (* Storing results *)
-  val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
+  val add_thmss: string -> string -> (Attrib.binding * (thm list * Token.src list) list) list ->
     Proof.context -> Proof.context
   val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
 
@@ -127,7 +127,7 @@
   (** dynamic part **)
   syntax_decls: (declaration * serial) list,
     (* syntax declarations *)
-  notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
+  notes: ((string * (Attrib.binding * (thm list * Token.src list) list) list) * serial) list,
     (* theorem declarations *)
   dependencies: ((string * (morphism * morphism)) * serial) list
     (* locale dependencies (sublocale relation) in reverse order *),
diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/method.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -41,15 +41,14 @@
   val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
   val tactic: Symbol_Pos.source -> Proof.context -> method
   val raw_tactic: Symbol_Pos.source -> Proof.context -> method
-  type src = Args.src
   type combinator_info
   val no_combinator_info: combinator_info
   datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int
   datatype text =
-    Source of src |
+    Source of Token.src |
     Basic of Proof.context -> method |
     Combinator of combinator_info * combinator * text list
-  val map_source: (src -> src) -> text -> text
+  val map_source: (Token.src -> Token.src) -> text -> text
   val primitive_text: (Proof.context -> thm -> thm) -> text
   val succeed_text: text
   val default_text: text
@@ -59,15 +58,16 @@
   val finish_text: text option * bool -> text
   val print_methods: Proof.context -> unit
   val check_name: Proof.context -> xstring * Position.T -> string
-  val method_syntax: (Proof.context -> method) context_parser -> Args.src -> Proof.context -> method
+  val method_syntax: (Proof.context -> method) context_parser ->
+    Token.src -> Proof.context -> method
   val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
   val local_setup: binding -> (Proof.context -> method) context_parser -> string ->
     local_theory -> local_theory
   val method_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
     local_theory -> local_theory
-  val method: Proof.context -> src -> Proof.context -> method
-  val method_closure: Proof.context -> src -> src
-  val method_cmd: Proof.context -> src -> Proof.context -> method
+  val method: Proof.context -> Token.src -> Proof.context -> method
+  val method_closure: Proof.context -> Token.src -> Token.src
+  val method_cmd: Proof.context -> Token.src -> Proof.context -> method
   val evaluate: text -> Proof.context -> method
   type modifier = (Proof.context -> Proof.context) * attribute
   val section: modifier parser list -> thm list context_parser
@@ -274,8 +274,6 @@
 
 (* method text *)
 
-type src = Args.src;
-
 datatype combinator_info = Combinator_Info of {keywords: Position.T list};
 fun combinator_info keywords = Combinator_Info {keywords = keywords};
 val no_combinator_info = combinator_info [];
@@ -283,7 +281,7 @@
 datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int;
 
 datatype text =
-  Source of src |
+  Source of Token.src |
   Basic of Proof.context -> method |
   Combinator of combinator_info * combinator * text list;
 
@@ -293,7 +291,7 @@
 
 fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r);
 val succeed_text = Basic (K succeed);
-val default_text = Source (Args.src ("default", Position.none) []);
+val default_text = Source (Token.src ("default", Position.none) []);
 val this_text = Basic (K this);
 val done_text = Basic (K (SIMPLE_METHOD all_tac));
 fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
@@ -307,7 +305,7 @@
 
 structure Methods = Generic_Data
 (
-  type T = ((src -> Proof.context -> method) * string) Name_Space.table;
+  type T = ((Token.src -> Proof.context -> method) * string) Name_Space.table;
   val empty : T = Name_Space.empty_table "method";
   val extend = I;
   fun merge data : T = Name_Space.merge_tables data;
@@ -354,13 +352,13 @@
 (* check *)
 
 fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
-fun check_src ctxt src = Args.check_src ctxt (get_methods ctxt) src;
+fun check_src ctxt src = Token.check_src ctxt (get_methods ctxt) src;
 
 
 (* method setup *)
 
 fun method_syntax scan src ctxt : method =
-  let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end;
+  let val (m, ctxt') = Token.syntax scan src ctxt in m ctxt' end;
 
 fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd;
 fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
@@ -379,15 +377,15 @@
 
 fun method ctxt =
   let val table = get_methods ctxt
-  in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
+  in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end;
 
 fun method_closure ctxt0 src0 =
   let
     val (src1, meth) = check_src ctxt0 src0;
-    val src2 = Args.init_assignable src1;
+    val src2 = Token.init_assignable_src src1;
     val ctxt = Context_Position.not_really ctxt0;
     val _ = Seq.pull (method ctxt src2 ctxt [] (Goal.protect 0 Drule.dummy_thm));
-  in Args.closure src2 end;
+  in Token.closure_src src2 end;
 
 fun method_cmd ctxt = method ctxt o method_closure ctxt;
 
@@ -505,9 +503,9 @@
 local
 
 fun meth4 x =
- (Parse.position Parse.xname >> (fn name => Source (Args.src name [])) ||
+ (Parse.position Parse.xname >> (fn name => Source (Token.src name [])) ||
   Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
-    Source (Args.src ("cartouche", Token.pos_of tok) [tok])) ||
+    Source (Token.src ("cartouche", Token.pos_of tok) [tok])) ||
   Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
 and meth3 x =
  (meth4 -- Parse.position (Parse.$$$ "?")
@@ -520,7 +518,7 @@
         Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) ||
   meth4) x
 and meth2 x =
- (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Args.src) ||
+ (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Token.src) ||
   meth3) x
 and meth1 x =
   (Parse.enum1_positions "," meth2
diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/parse.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -6,8 +6,6 @@
 
 signature PARSE =
 sig
-  type 'a parser = Token.T list -> 'a * Token.T list
-  type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list)
   val group: (unit -> string) -> (Token.T list -> 'a) -> Token.T list -> 'a
   val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
   val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
@@ -114,10 +112,6 @@
 structure Parse: PARSE =
 struct
 
-type 'a parser = Token.T list -> 'a * Token.T list;
-type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list);
-
-
 (** error handling **)
 
 (* group atomic parsers (no cuts!) *)
@@ -441,6 +435,3 @@
 
 end;
 
-type 'a parser = 'a Parse.parser;
-type 'a context_parser = 'a Parse.context_parser;
-
diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -6,17 +6,17 @@
 
 signature PARSE_SPEC =
 sig
-  val attribs: Attrib.src list parser
-  val opt_attribs: Attrib.src list parser
+  val attribs: Token.src list parser
+  val opt_attribs: Token.src list parser
   val thm_name: string -> Attrib.binding parser
   val opt_thm_name: string -> Attrib.binding parser
   val spec: (Attrib.binding * string) parser
   val specs: (Attrib.binding * string list) parser
   val alt_specs: (Attrib.binding * string) list parser
   val where_alt_specs: (Attrib.binding * string) list parser
-  val xthm: (Facts.ref * Attrib.src list) parser
-  val xthms1: (Facts.ref * Attrib.src list) list parser
-  val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
+  val xthm: (Facts.ref * Token.src list) parser
+  val xthms1: (Facts.ref * Token.src list) list parser
+  val name_facts: (Attrib.binding * (Facts.ref * Token.src list) list) list parser
   val constdecl: (binding * string option * mixfix) parser
   val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
   val includes: (xstring * Position.T) list parser
@@ -37,7 +37,7 @@
 
 (* theorem specifications *)
 
-val attrib = Parse.position Parse.liberal_name -- Parse.!!! Parse.args >> uncurry Args.src;
+val attrib = Parse.position Parse.liberal_name -- Parse.!!! Parse.args >> uncurry Token.src;
 val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
 val opt_attribs = Scan.optional attribs [];
 
diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -61,18 +61,18 @@
   val chain: state -> state
   val chain_facts: thm list -> state -> state
   val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
-  val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
+  val note_thmss_cmd: (Attrib.binding * (Facts.ref * Token.src list) list) list -> state -> state
   val from_thmss: ((thm list * attribute list) list) list -> state -> state
-  val from_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+  val from_thmss_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
   val with_thmss: ((thm list * attribute list) list) list -> state -> state
-  val with_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+  val with_thmss_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
   val using: ((thm list * attribute list) list) list -> state -> state
-  val using_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+  val using_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
   val unfolding: ((thm list * attribute list) list) list -> state -> state
-  val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+  val unfolding_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
   val invoke_case: (string * Position.T) * binding option list * attribute list ->
     state -> state
-  val invoke_case_cmd: (string * Position.T) * binding option list * Attrib.src list ->
+  val invoke_case_cmd: (string * Position.T) * binding option list * Token.src list ->
     state -> state
   val begin_block: state -> state
   val next_block: state -> state
diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/specification.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -51,11 +51,11 @@
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   val theorems: string ->
-    (Attrib.binding * (thm list * Attrib.src list) list) list ->
+    (Attrib.binding * (thm list * Token.src list) list) list ->
     (binding * typ option * mixfix) list ->
     bool -> local_theory -> (string * thm list) list * local_theory
   val theorems_cmd: string ->
-    (Attrib.binding * (Facts.ref * Attrib.src list) list) list ->
+    (Attrib.binding * (Facts.ref * Token.src list) list) list ->
     (binding * string option * mixfix) list ->
     bool -> local_theory -> (string * thm list) list * local_theory
   val theorem: string -> Method.text option ->
diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/token.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -66,10 +66,22 @@
   val mk_term: term -> T
   val mk_fact: string option * thm list -> T
   val mk_attribute: (morphism -> attribute) -> T
-  val transform_value: morphism -> T -> T
+  val transform: morphism -> T -> T
   val init_assignable: T -> T
   val assign: value option -> T -> unit
   val closure: T -> T
+
+  type src
+  val src: xstring * Position.T -> T list -> src
+  val name_of_src: src -> string * Position.T
+  val range_of_src: src -> Position.T
+  val unparse_src: src -> string list
+  val pretty_src: Proof.context -> src -> Pretty.T
+  val check_src: Proof.context -> 'a Name_Space.table -> src -> src * 'a
+  val transform_src: morphism -> src -> src
+  val init_assignable_src: src -> src
+  val closure_src: src -> src
+
   val ident_or_symbolic: string -> bool
   val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
   val source': {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
@@ -78,6 +90,11 @@
     Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
   val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a
+
+  type 'a parser = T list -> 'a * T list
+  type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
+  val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
+  val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
 end;
 
 structure Token: TOKEN =
@@ -378,7 +395,7 @@
 
 (* transform value *)
 
-fun transform_value phi =
+fun transform phi =
   map_value (fn v =>
     (case v of
       Literal _ => v
@@ -407,6 +424,58 @@
 
 
 
+(** src **)
+
+datatype src =
+  Src of
+   {name: string * Position.T,
+    args: T list,
+    output_info: (string * Markup.T) option};
+
+fun src name args = Src {name = name, args = args, output_info = NONE};
+
+fun name_of_src (Src {name, ...}) = name;
+
+fun range_of_src (Src {name = (_, pos), args, ...}) =
+  if null args then pos
+  else Position.set_range (pos, #2 (range_of args));
+
+fun unparse_src (Src {args, ...}) = map unparse args;
+
+fun pretty_src ctxt src =
+  let
+    val Src {name = (name, _), args, output_info} = src;
+    val prt_name =
+      (case output_info of
+        NONE => Pretty.str name
+      | SOME (_, markup) => Pretty.mark_str (markup, name));
+    val prt_arg = pretty_value ctxt;
+  in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
+
+
+(* check *)
+
+fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) =
+  let
+    val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
+    val space = Name_Space.space_of_table table;
+    val kind = Name_Space.kind_of space;
+    val markup = Name_Space.markup space name;
+  in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end;
+
+
+(* values *)
+
+fun map_args f (Src {name, args, output_info}) =
+  Src {name = name, args = map f args, output_info = output_info};
+
+val transform_src = map_args o transform;
+
+val init_assignable_src = map_args init_assignable;
+val closure_src = map_args closure;
+
+
+
 (** scanners **)
 
 open Basic_Symbol_Pos;
@@ -546,4 +615,44 @@
       |> Source.exhaust;
   in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
 
+
+
+(** parsers **)
+
+type 'a parser = T list -> 'a * T list;
+type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list);
+
+fun syntax_generic scan (Src {name = (name, pos), args = args0, output_info}) context =
+  let
+    val args1 = map init_assignable args0;
+    fun reported_text () =
+      if Context_Position.is_visible_generic context then
+        ((pos, Markup.operator) :: maps (reports_of_value o closure) args1)
+        |> map (fn (p, m) => Position.reported_text p m "")
+      else [];
+  in
+    (case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of
+      (SOME x, (context', [])) =>
+        let val _ = Output.report (reported_text ())
+        in (x, context') end
+    | (_, (_, args2)) =>
+        let
+          val print_name =
+            (case output_info of
+              NONE => quote name
+            | SOME (kind, markup) => plain_words kind ^ " " ^ quote (Markup.markup markup name));
+          val print_args =
+            if null args2 then "" else ":\n  " ^ space_implode " " (map print args2);
+        in
+          error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^
+            Markup.markup_report (implode (reported_text ())))
+        end)
+  end;
+
+fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof;
+
 end;
+
+type 'a parser = 'a Token.parser;
+type 'a context_parser = 'a Token.context_parser;
+
diff -r 568840962230 -r bc6bced136e5 src/Pure/ML/ml_antiquotation.ML
--- a/src/Pure/ML/ml_antiquotation.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -8,7 +8,7 @@
 sig
   val variant: string -> Proof.context -> string * Proof.context
   val declaration: binding -> 'a context_parser ->
-    (Args.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
+    (Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
     theory -> theory
   val inline: binding -> string context_parser -> theory -> theory
   val value: binding -> string context_parser -> theory -> theory
@@ -40,7 +40,7 @@
 fun declaration name scan body =
   ML_Context.add_antiquotation name
     (fn src => fn orig_ctxt =>
-      let val (x, _) = Args.syntax scan src orig_ctxt
+      let val (x, _) = Token.syntax scan src orig_ctxt
       in body src x orig_ctxt end);
 
 fun inline name scan =
@@ -62,7 +62,7 @@
     (fn src => fn () => fn ctxt =>
       let
         val (a, ctxt') = variant "position" ctxt;
-        val (_, pos) = Args.name_of_src src;
+        val (_, pos) = Token.name_of_src src;
         val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n";
         val body = "Isabelle." ^ a;
       in (K (env, body), ctxt') end) #>
diff -r 568840962230 -r bc6bced136e5 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -64,7 +64,7 @@
     (Scan.lift (Scan.optional Args.name "Output.writeln"))
       (fn src => fn output => fn ctxt =>
         let
-          val (_, pos) = Args.name_of_src src;
+          val (_, pos) = Token.name_of_src src;
           val (a, ctxt') = ML_Antiquotation.variant "output" ctxt;
           val env =
             "val " ^ a ^ ": string -> unit =\n\
diff -r 568840962230 -r bc6bced136e5 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/ML/ml_context.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -14,7 +14,7 @@
   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 ->
@@ -55,7 +55,7 @@
 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;
@@ -75,7 +75,7 @@
   |> 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;
 
 
@@ -85,7 +85,7 @@
 
 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";
 
diff -r 568840962230 -r bc6bced136e5 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/ML/ml_thms.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -6,7 +6,7 @@
 
 signature ML_THMS =
 sig
-  val the_attributes: Proof.context -> int -> Args.src list
+  val the_attributes: Proof.context -> int -> Token.src list
   val the_thmss: Proof.context -> thm list list
   val get_stored_thms: unit -> thm list
   val get_stored_thm: unit -> thm
@@ -25,7 +25,7 @@
 
 structure Data = Proof_Data
 (
-  type T = Args.src list Inttab.table * thms list;
+  type T = Token.src list Inttab.table * thms list;
   fun init _ = (Inttab.empty, []);
 );
 
diff -r 568840962230 -r bc6bced136e5 src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Thy/term_style.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -35,8 +35,8 @@
 fun parse_single ctxt =
   Parse.position Parse.xname -- Parse.args >> (fn (name, args) =>
     let
-      val (src, parse) = Args.check_src ctxt (get_data ctxt) (Args.src name args);
-      val (f, _) = Args.syntax (Scan.lift parse) src ctxt;
+      val (src, parse) = Token.check_src ctxt (get_data ctxt) (Token.src name args);
+      val (f, _) = Token.syntax (Scan.lift parse) src ctxt;
     in f ctxt end);
 
 val parse = Args.context :|-- (fn ctxt => Scan.lift
diff -r 568840962230 -r bc6bced136e5 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Thy/thy_output.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -18,7 +18,7 @@
   val check_option: Proof.context -> xstring * Position.T -> string
   val print_antiquotations: Proof.context -> unit
   val antiquotation: binding -> 'a context_parser ->
-    ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
+    ({source: Token.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
       theory -> theory
   val boolean: string -> bool
   val integer: string -> int
@@ -30,9 +30,9 @@
   val pretty_text: Proof.context -> string -> Pretty.T
   val pretty_term: Proof.context -> term -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
-  val str_of_source: Args.src -> string
+  val str_of_source: Token.src -> string
   val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
-    Args.src -> 'a list -> Pretty.T list
+    Token.src -> 'a list -> Pretty.T list
   val output: Proof.context -> Pretty.T list -> string
   val verb_text: string -> string
 end;
@@ -67,7 +67,7 @@
 structure Antiquotations = Theory_Data
 (
   type T =
-    (Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
+    (Token.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
       (string -> Proof.context -> Proof.context) Name_Space.table;
   val empty : T =
     (Name_Space.empty_table Markup.document_antiquotationN,
@@ -91,7 +91,7 @@
 fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
 
 fun command src state ctxt =
-  let val (src', f) = Args.check_src ctxt (#1 (get_antiquotations ctxt)) src
+  let val (src', f) = Token.check_src ctxt (#1 (get_antiquotations ctxt)) src
   in f src' state ctxt end;
 
 fun option ((xname, pos), s) ctxt =
@@ -114,7 +114,7 @@
 fun antiquotation name scan body =
   add_command name
     (fn src => fn state => fn ctxt =>
-      let val (x, ctxt') = Args.syntax scan src ctxt
+      let val (x, ctxt') = Token.syntax scan src ctxt
       in body {source = src, state = state, context = ctxt'} x end);
 
 
@@ -151,7 +151,7 @@
 val antiq =
   Parse.!!!
     (Parse.position Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
-  >> (fn ((name, props), args) => (props, Args.src name args));
+  >> (fn ((name, props), args) => (props, Token.src name args));
 
 end;
 
@@ -534,7 +534,7 @@
 
 (* default output *)
 
-val str_of_source = space_implode " " o Args.unparse_src;
+val str_of_source = space_implode " " o Token.unparse_src;
 
 fun maybe_pretty_source pretty ctxt src xs =
   map (pretty ctxt) xs  (*always pretty in order to exhibit errors!*)
@@ -624,7 +624,7 @@
       Scan.lift (Parse.position (Args.$$$ "by") -- Method.parse -- Scan.option Method.parse))
     (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
       let
-        val prop_src = Args.src (Args.name_of_src source) [prop_token];
+        val prop_src = Token.src (Token.name_of_src source) [prop_token];
 
         val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
         val _ = Context_Position.reports ctxt reports;
diff -r 568840962230 -r bc6bced136e5 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -32,8 +32,8 @@
   val add_datatype_i: term * term list -> Ind_Syntax.constructor_spec list list ->
     thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
   val add_datatype: string * string list -> (string * string list * mixfix) list list ->
-    (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
-    (Facts.ref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result
+    (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list *
+    (Facts.ref * Token.src list) list -> theory -> theory * inductive_result * datatype_result
 end;
 
 functor Add_datatype_def_Fun
diff -r 568840962230 -r bc6bced136e5 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -12,8 +12,8 @@
   val induct_tac: Proof.context -> string -> int -> tactic
   val exhaust_tac: Proof.context -> string -> int -> tactic
   val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
-  val rep_datatype: Facts.ref * Attrib.src list -> Facts.ref * Attrib.src list ->
-    (Facts.ref * Attrib.src list) list -> (Facts.ref * Attrib.src list) list -> theory -> theory
+  val rep_datatype: Facts.ref * Token.src list -> Facts.ref * Token.src list ->
+    (Facts.ref * Token.src list) list -> (Facts.ref * Token.src list) list -> theory -> theory
   val setup: theory -> theory
 end;
 
diff -r 568840962230 -r bc6bced136e5 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -29,9 +29,9 @@
     ((binding * term) * attribute list) list ->
     thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
   val add_inductive: string list * string ->
-    ((binding * string) * Attrib.src list) list ->
-    (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
-    (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list ->
+    ((binding * string) * Token.src list) list ->
+    (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list *
+    (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list ->
     theory -> theory * inductive_result
 end;
 
diff -r 568840962230 -r bc6bced136e5 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -8,7 +8,7 @@
 
 signature PRIMREC_PACKAGE =
 sig
-  val add_primrec: ((binding * string) * Attrib.src list) list -> theory -> theory * thm list
+  val add_primrec: ((binding * string) * Token.src list) list -> theory -> theory * thm list
   val add_primrec_i: ((binding * term) * attribute list) list -> theory -> theory * thm list
 end;