Context.generic is canonical state of parsers;
removed obsolete global/local parsers;
tuned interfaces;

--- a/src/Pure/Isar/args.ML	Fri Feb 10 02:22:39 2006 +0100
+++ b/src/Pure/Isar/args.ML	Fri Feb 10 02:22:41 2006 +0100
@@ -69,31 +69,21 @@
   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 global_typ_abbrev: theory * T list -> typ * (theory * T list)
-  val global_typ: theory * T list -> typ * (theory * T list)
-  val global_term: theory * T list -> term * (theory * T list)
-  val global_prop: theory * T list -> term * (theory * T list)
-  val local_typ_abbrev: ProofContext.context * T list -> typ * (ProofContext.context * T list)
-  val local_typ: ProofContext.context * T list -> typ * (ProofContext.context * T list)
-  val local_term: ProofContext.context * T list -> term * (ProofContext.context * T list)
-  val local_prop: ProofContext.context * T list -> term * (ProofContext.context * 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 prop: Context.generic * T list -> term * (Context.generic * T list)
-  val global_tyname: theory * T list -> string * (theory * T list)
-  val global_const: theory * T list -> string * (theory * T list)
-  val local_tyname: ProofContext.context * T list -> string * (ProofContext.context * T list)
-  val local_const: ProofContext.context * T list -> string * (ProofContext.context * 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 thm_sel: T list -> PureThy.interval list * T list
-  val bang_facts: ProofContext.context * T list -> thm list * (ProofContext.context * 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 attribs: (string -> string) -> T list -> src list * T list
   val opt_attribs: (string -> string) -> T list -> src list * T list
-  val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> src -> 'a -> 'a * 'b
+  val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'b * 'a
+  val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
+    src -> ProofContext.context -> ProofContext.context * 'a
   val pretty_src: ProofContext.context -> src -> Pretty.T
   val pretty_attribs: ProofContext.context -> src list -> Pretty.T list
 end;
@@ -307,16 +297,6 @@
 
 (* terms and types *)
 
-val global_typ_abbrev = Scan.peek (named_typ o ProofContext.read_typ_abbrev o ProofContext.init);
-val global_typ = Scan.peek (named_typ o ProofContext.read_typ o ProofContext.init);
-val global_term = Scan.peek (named_term o ProofContext.read_term o ProofContext.init);
-val global_prop = Scan.peek (named_term o ProofContext.read_prop o ProofContext.init);
-
-val local_typ_abbrev = Scan.peek (named_typ o ProofContext.read_typ_abbrev);
-val local_typ = Scan.peek (named_typ o ProofContext.read_typ);
-val local_term = Scan.peek (named_term o ProofContext.read_term);
-val local_prop = Scan.peek (named_term o ProofContext.read_prop);
-
 val typ_abbrev = Scan.peek (named_typ o ProofContext.read_typ_abbrev o Context.proof_of);
 val typ = Scan.peek (named_typ o ProofContext.read_typ o Context.proof_of);
 val term = Scan.peek (named_term o ProofContext.read_term o Context.proof_of);
@@ -325,17 +305,11 @@
 
 (* type and constant names *)
 
-val dest_tyname = fn Type (c, _) => c | TFree (a, _) => a | _ => "";
-val dest_const = fn Const (c, _) => c | Free (x, _) => x | _ => "";
+val tyname = Scan.peek (named_typ o Context.cases Sign.read_tyname ProofContext.read_tyname)
+  >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
 
-val global_tyname = Scan.peek (named_typ o Sign.read_tyname) >> dest_tyname;
-val global_const = Scan.peek (named_term o Sign.read_const) >> dest_const;
-val local_tyname = Scan.peek (named_typ o ProofContext.read_tyname) >> dest_tyname;
-val local_const = Scan.peek (named_term o ProofContext.read_const) >> dest_const;
-val tyname =
-  Scan.peek (named_typ o Context.cases Sign.read_tyname ProofContext.read_tyname) >> dest_tyname;
-val const =
-  Scan.peek (named_term o Context.cases Sign.read_const ProofContext.read_const) >> dest_const;
+val const = Scan.peek (named_term o Context.cases Sign.read_const ProofContext.read_const)
+  >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
 
 
 (* misc *)
@@ -345,8 +319,8 @@
   nat --| $$$ "-" >> PureThy.From ||
   nat >> PureThy.Single));
 
-val bang_facts = Scan.peek (fn ctxt =>
-  $$$ "!" >> K (ProofContext.prems_of ctxt) || Scan.succeed []);
+val bang_facts = Scan.peek (fn context =>
+  $$$ "!" >> K (ProofContext.prems_of (Context.proof_of context)) || Scan.succeed []);
 
 
 (* goal specification *)
@@ -404,6 +378,8 @@
       error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": bad arguments\n  " ^
         space_implode " " (map string_of args')));
 
+fun context_syntax kind scan src = apfst Context.the_proof o syntax kind scan src o Context.Proof;
+
 
 
 (** pretty printing **)

--- a/src/Pure/Isar/attrib.ML	Fri Feb 10 02:22:39 2006 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Feb 10 02:22:41 2006 +0100
@@ -27,15 +27,9 @@
     (('c * 'att list) * ('d * 'att list) list) list
   val crude_closure: Context.proof -> src -> src
   val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
-  val global_thm: theory * Args.T list -> thm * (theory * Args.T list)
-  val global_thms: theory * Args.T list -> thm list * (theory * Args.T list)
-  val global_thmss: theory * Args.T list -> thm list * (theory * Args.T list)
-  val local_thm: Context.proof * Args.T list -> thm * (Context.proof * Args.T list)
-  val local_thms: Context.proof * Args.T list -> thm list * (Context.proof * Args.T list)
-  val local_thmss: Context.proof * Args.T list -> thm list * (Context.proof * 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 thmss: 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 syntax: (Context.generic * Args.T list ->
     attribute * (Context.generic * Args.T list)) -> src -> attribute
   val no_args: attribute -> src -> attribute
@@ -149,37 +143,28 @@
 
 local
 
-fun gen_thm theory_of apply get pick = Scan.depend (fn st =>
- (Scan.ahead Args.alt_name -- Args.named_fact (get st o Fact)
+val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms;
+
+fun gen_thm pick = Scan.depend (fn st =>
+ (Scan.ahead Args.alt_name -- Args.named_fact (get_thms st o Fact)
     >> (fn (s, fact) => ("", Fact s, fact)) ||
-  Scan.ahead Args.name -- Args.named_fact (get st o Name) -- Args.thm_sel
+  Scan.ahead Args.name -- Args.named_fact (get_thms st o Name) -- Args.thm_sel
     >> (fn ((name, fact), sel) => (name, NameSelection (name, sel), fact)) ||
-  Scan.ahead Args.name -- Args.named_fact (get st o Name)
+  Scan.ahead Args.name -- Args.named_fact (get_thms st o Name)
     >> (fn (name, fact) => (name, Name name, fact))) --
-  Args.opt_attribs (intern (theory_of st))
+  Args.opt_attribs (intern (Context.theory_of st))
   >> (fn ((name, thmref, fact), srcs) =>
     let
       val ths = PureThy.select_thm thmref fact;
-      val atts = map (attribute_i (theory_of st)) srcs;
-      val (st', ths') = foldl_map (apply atts) (st, ths);
+      val atts = map (attribute_i (Context.theory_of st)) srcs;
+      val (st', ths') = foldl_map (Library.apply atts) (st, ths);
     in (st', pick name ths') end));
 
-val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms;
-
 in
 
-val global_thm = gen_thm I Thm.theory_attributes PureThy.get_thms PureThy.single_thm;
-val global_thms = gen_thm I Thm.theory_attributes PureThy.get_thms (K I);
-val global_thmss = Scan.repeat global_thms >> List.concat;
-
-val local_thm =
-  gen_thm ProofContext.theory_of Thm.proof_attributes ProofContext.get_thms PureThy.single_thm;
-val local_thms = gen_thm ProofContext.theory_of Thm.proof_attributes ProofContext.get_thms (K I);
-val local_thmss = Scan.repeat local_thms >> List.concat;
-
-val thm = gen_thm Context.theory_of Library.apply get_thms PureThy.single_thm;
-val thms = gen_thm Context.theory_of Library.apply get_thms (K I);
-val thmss = Scan.repeat thms >> List.concat;
+val thm = gen_thm PureThy.single_thm;
+val multi_thm = gen_thm (K I);
+val thms = Scan.repeat multi_thm >> List.concat;
 
 end;
 
@@ -217,7 +202,7 @@
     >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B))));
 
 val OF_att =
-  syntax (thmss >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A)));
+  syntax (thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A)));
 
 
 (* read_instantiate: named instantiation of type and term variables *)
@@ -397,7 +382,7 @@
 (* unfold / fold definitions *)
 
 fun unfolded_syntax rule =
-  syntax (thmss >>
+  syntax (thms >>
     (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths)));
 
 val unfolded = unfolded_syntax LocalDefs.unfold;