# HG changeset patch
# User wenzelm
# Date 1139534536 -3600
# Node ID d6e5fa2ba8b8779502804240037c752942bc9ae8
# Parent  61c7875a58b81cc120f040aeacd01425dc204ccc
Args/Attrib syntax: Context.generic;

diff -r 61c7875a58b8 -r d6e5fa2ba8b8 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Fri Feb 10 02:22:13 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Fri Feb 10 02:22:16 2006 +0100
@@ -262,7 +262,7 @@
 local
 
 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
-val opt_rule = Scan.option (rule_spec |-- Attrib.local_thm);
+val opt_rule = Scan.option (rule_spec |-- Attrib.thm);
 
 val varss =
   Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
diff -r 61c7875a58b8 -r d6e5fa2ba8b8 src/Provers/eqsubst.ML
--- a/src/Provers/eqsubst.ML	Fri Feb 10 02:22:13 2006 +0100
+++ b/src/Provers/eqsubst.ML	Fri Feb 10 02:22:16 2006 +0100
@@ -331,7 +331,7 @@
 should be done to an assumption, false = apply to the conclusion of
 the goal) as well as the theorems to use *)
 fun subst_meth src =
-  Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.local_thms) src
+  Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
   #> (fn (ctxt, ((asmflag, occL), inthms)) =>
     (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
 
diff -r 61c7875a58b8 -r d6e5fa2ba8b8 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Fri Feb 10 02:22:13 2006 +0100
+++ b/src/Provers/induct_method.ML	Fri Feb 10 02:22:16 2006 +0100
@@ -491,29 +491,29 @@
 
 fun named_rule k arg get =
   Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :--
-    (fn names => Scan.peek (fn ctxt => Scan.succeed (names |> map (fn name =>
-      (case get ctxt name of SOME x => x
+    (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
+      (case get (Context.proof_of context) name of SOME x => x
       | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))) >> #2;
 
 fun rule get_type get_set =
-  named_rule InductAttrib.typeN Args.local_tyname get_type ||
-  named_rule InductAttrib.setN Args.local_const get_set ||
-  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thmss;
+  named_rule InductAttrib.typeN Args.tyname get_type ||
+  named_rule InductAttrib.setN Args.const get_set ||
+  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
 
 val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS >> single_rule;
 val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS;
 val coinduct_rule =
   rule InductAttrib.lookup_coinductT InductAttrib.lookup_coinductS >> single_rule;
 
-val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.local_term >> SOME;
+val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
 
 val def_inst =
   ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
-      -- Args.local_term) >> SOME ||
+      -- Args.term) >> SOME ||
     inst >> Option.map (pair NONE);
 
-val free = Scan.state -- Args.local_term >> (fn (_, Free v) => v | (ctxt, t) =>
-  error ("Bad free variable: " ^ ProofContext.string_of_term ctxt t));
+val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) =>
+  error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t));
 
 fun unless_more_args scan = Scan.unless (Scan.lift
   ((Args.$$$ fixingN || Args.$$$ takingN || Args.$$$ InductAttrib.typeN ||
diff -r 61c7875a58b8 -r d6e5fa2ba8b8 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Fri Feb 10 02:22:13 2006 +0100
+++ b/src/Provers/splitter.ML	Fri Feb 10 02:22:16 2006 +0100
@@ -448,7 +448,7 @@
   Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
 
 fun split_meth src =
-  Method.syntax Attrib.local_thms src
+  Method.syntax Attrib.thms src
   #> (fn (_, ths) => Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths));
 
 
diff -r 61c7875a58b8 -r d6e5fa2ba8b8 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Fri Feb 10 02:22:13 2006 +0100
+++ b/src/Pure/Isar/isar_output.ML	Fri Feb 10 02:22:16 2006 +0100
@@ -16,7 +16,7 @@
   val print_antiquotations: unit -> unit
   val boolean: string -> bool
   val integer: string -> int
-  val args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
+  val args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
     (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
   datatype markup = Markup | MarkupEnv | Verbatim
   val modes: string list ref
@@ -110,8 +110,7 @@
 
 (* args syntax *)
 
-fun syntax (scan: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))) =
-  Args.syntax "antiquotation" scan;
+fun syntax scan = Args.context_syntax "antiquotation" scan;
 
 fun args scan f src state : string =
   let
@@ -505,20 +504,20 @@
 (* commands *)
 
 val _ = add_commands
- [("thm", args Attrib.local_thmss (output_list pretty_thm)),
-  ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.local_thm) (output pretty_thm_style)),
-  ("prop", args Args.local_prop (output pretty_term)),
-  ("term", args Args.local_term (output pretty_term)),
-  ("term_style", args (Scan.lift Args.liberal_name -- Args.local_term) (output pretty_term_style)),
-  ("term_type", args Args.local_term (output pretty_term_typ)),
-  ("typeof", args Args.local_term (output pretty_term_typeof)),
-  ("const", args Args.local_term (output pretty_term_const)),
-  ("typ", args Args.local_typ_abbrev (output ProofContext.pretty_typ)),
+ [("thm", args Attrib.thms (output_list pretty_thm)),
+  ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.thm) (output pretty_thm_style)),
+  ("prop", args Args.prop (output pretty_term)),
+  ("term", args Args.term (output pretty_term)),
+  ("term_style", args (Scan.lift Args.liberal_name -- Args.term) (output pretty_term_style)),
+  ("term_type", args Args.term (output pretty_term_typ)),
+  ("typeof", args Args.term (output pretty_term_typeof)),
+  ("const", args Args.term (output pretty_term_const)),
+  ("typ", args Args.typ_abbrev (output ProofContext.pretty_typ)),
   ("text", args (Scan.lift Args.name) (output (K pretty_text))),
   ("goals", output_goals true),
   ("subgoals", output_goals false),
-  ("prf", args Attrib.local_thmss (output (pretty_prf false))),
-  ("full_prf", args Attrib.local_thmss (output (pretty_prf true))),
+  ("prf", args Attrib.thms (output (pretty_prf false))),
+  ("full_prf", args Attrib.thms (output (pretty_prf true))),
   ("ML", args (Scan.lift Args.name) (output_ml ml_val)),
   ("ML_type", args (Scan.lift Args.name) (output_ml ml_type)),
   ("ML_struct", args (Scan.lift Args.name) (output_ml ml_struct))];
diff -r 61c7875a58b8 -r d6e5fa2ba8b8 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Feb 10 02:22:13 2006 +0100
+++ b/src/Pure/simplifier.ML	Fri Feb 10 02:22:16 2006 +0100
@@ -251,7 +251,7 @@
 in
 
 val simplified =
-  Attrib.syntax (conv_mode -- Attrib.thmss >> (fn (f, ths) => Thm.rule_attribute (fn x =>
+  Attrib.syntax (conv_mode -- Attrib.thms >> (fn (f, ths) => Thm.rule_attribute (fn x =>
     f ((if null ths then I else MetaSimplifier.clear_ss) (get_ss x) addsimps ths))));
 
 end;