src/Pure/Isar/args.ML

   val global_prop: theory * T list -> term * (theory * T list)
   val local_typ: Proof.context * T list -> typ * (Proof.context * T list)
   val local_term: Proof.context * T list -> term * (Proof.context * T list)
   val local_prop: Proof.context * T list -> term * (Proof.context * T list)
   val bang_facts: Proof.context * T list -> thm list * (Proof.context * T list)
+  val goal_spec: T list -> ((int -> tactic) -> tactic) * T list
   type src
   val src: (string * T list) * Position.T -> src
   val dest_src: src -> (string * T list) * Position.T
   val attribs: T list -> src list * T list
   val opt_attribs: T list -> src list * T list

 fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
 fun $$$ x = $$$$ x >> val_of;
 
 val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
 
+val keyword_symid =
+  Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of;
+
 fun kind f = Scan.one (K true) :--
   (fn Arg (Ident, (x, _)) =>
     (case f x of Some y => Scan.succeed y | _ => Scan.fail)
   | _ => Scan.fail) >> #2;
 

 
 (* bang facts *)
 
 val bang_facts = Scan.depend (fn ctxt =>
   ($$$ "!" >> K (ProofContext.prems_of ctxt) || Scan.succeed []) >> pair ctxt);
+
+
+(* goal specifier *)
+
+val tactical = $$$$ "!" >> K ALLGOALS || $$$$ "?" >> K FINDGOAL || nat >> curry op |>;
+val goal_spec = $$$$ "(" |-- tactical --| $$$$ ")";
 
 
 (* args *)
 
 val exclude = explode "(){}[],";

 (* attribs *)
 
 fun list1 scan = scan -- Scan.repeat ($$$ "," |-- scan) >> op ::;
 fun list scan = list1 scan || Scan.succeed [];
 
-val attrib = position (name -- !!! (args false)) >> src;
+val attrib = position ((keyword_symid || name) -- !!! (args false)) >> src;
 val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
 val opt_attribs = Scan.optional attribs [];
 
 
 end;