src/Pure/Isar/method.ML

   val goal_args_ctxt: (Args.T list -> 'a * Args.T list) ->
     (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method
   val goal_args_ctxt': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
     (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method
   val parse: OuterLex.token list -> text * OuterLex.token list
-  val parse_args: Args.T list -> text * Args.T list
 end;
 
 structure Method: METHOD =
 struct
 

 
 
 
 (** concrete syntax **)
 
+structure P = OuterParse;
+
+
 (* basic *)
 
 fun syntax scan = Args.context_syntax "method" scan;
 
 fun simple_args scan f src ctxt : method =

 val elimN = "elim";
 val destN = "dest";
 val ruleN = "rule";
 
 fun modifier name kind kind' att =
-  Args.$$$ name |-- (kind >> K NONE || kind' |-- Args.nat --| Args.colon >> SOME)
+  Args.$$$ name |-- (kind >> K NONE || kind' |-- P.nat --| Args.colon >> SOME)
     >> (pair (I: Proof.context -> Proof.context) o att);
 
 val iprover_modifiers =
  [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang,
   modifier destN Args.colon (Scan.succeed ()) ContextRules.dest,

   Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
 
 in
 
 val iprover_meth =
-  bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option Args.nat))
+  bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option P.nat))
     (fn n => fn prems => fn ctxt => METHOD (fn facts =>
       HEADGOAL (insert_tac (prems @ facts) THEN'
       ObjectLogic.atomize_prems_tac THEN' iprover_tac ctxt n)));
 
 end;
 
 
 (* tactic syntax *)
 
 fun nat_thms_args f = uncurry f oo
-  (fst oo syntax (Scan.lift (Scan.optional (Args.parens Args.nat) 0) -- Attrib.thms));
+  (fst oo syntax (Scan.lift (Scan.optional (Args.parens P.nat) 0) -- Attrib.thms));
 
 fun goal_args' args tac src ctxt = fst (syntax (Args.goal_spec HEADGOAL -- args >>
   (fn (quant, s) => SIMPLE_METHOD'' quant (tac s))) src ctxt);
 
 fun goal_args args tac = goal_args' (Scan.lift args) tac;

 fun goal_args_ctxt' args tac src ctxt =
   fst (syntax (Args.goal_spec HEADGOAL -- args >>
   (fn (quant, s) => SIMPLE_METHOD'' quant (tac ctxt s))) src ctxt);
 
 fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac;
+
+
+(* outer parser *)
+
+fun is_symid_meth s =
+  s <> "|" andalso s <> "?" andalso s <> "+" andalso OuterLex.ident_or_symbolic s;
+
+local
+
+fun meth4 x =
+ (P.position (P.xname >> rpair []) >> (Source o Args.src) ||
+  P.$$$ "(" |-- P.!!! (meth0 --| P.$$$ ")")) x
+and meth3 x =
+ (meth4 --| P.$$$ "?" >> Try ||
+  meth4 --| P.$$$ "+" >> Repeat1 ||
+  meth4 -- (P.$$$ "[" |-- Scan.optional P.nat 1 --| P.$$$ "]") >> (SelectGoals o swap) ||
+  meth4) x
+and meth2 x =
+ (P.position (P.xname -- Args.parse1 is_symid_meth) >> (Source o Args.src) ||
+  meth3) x
+and meth1 x = (P.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
+and meth0 x = (P.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
+
+in val parse = meth3 end;
 
 
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory

     ("this", no_args this, "apply current facts as rules"),
     ("fact", thms_ctxt_args fact, "composition by facts from context"),
     ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
     ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_tac,
       "rename parameters of goal"),
-    ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
+    ("rotate_tac", goal_args (Scan.optional P.int 1) Tactic.rotate_tac,
       "rotate assumptions of goal"),
-    ("tactic", simple_args (Args.position Args.name) tactic, "ML tactic as proof method"),
-    ("raw_tactic", simple_args (Args.position Args.name) raw_tactic,
+    ("tactic", simple_args (P.position Args.name) tactic, "ML tactic as proof method"),
+    ("raw_tactic", simple_args (P.position Args.name) raw_tactic,
       "ML tactic as raw proof method")]));
-
-
-(* outer parser *)
-
-structure T = OuterLex;
-structure P = OuterParse;
-
-fun is_symid_meth s =
-  s <> "|" andalso s <> "?" andalso s <> "+" andalso T.is_sid s;
-
-local
-
-fun meth4 x =
- (P.position (P.xname >> rpair []) >> (Source o Args.src) ||
-  P.$$$ "(" |-- P.!!! (meth0 --| P.$$$ ")")) x
-and meth3 x =
- (meth4 --| P.$$$ "?" >> Try ||
-  meth4 --| P.$$$ "+" >> Repeat1 ||
-  meth4 -- (P.$$$ "[" |-- Scan.optional P.nat 1 --| P.$$$ "]") >> (SelectGoals o swap) ||
-  meth4) x
-and meth2 x =
- (P.position (P.xname -- P.generic_args1 is_symid_meth) >> (Source o Args.src) ||
-  meth3) x
-and meth1 x = (P.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
-and meth0 x = (P.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
-
-in val parse = meth3 end;
-
-
-(* args parser *)
-
-local
-
-fun enum1 sep scan = scan ::: Scan.repeat (Args.$$$ sep |-- scan);
-
-fun meth4 x =
- (Args.position (Args.name >> rpair []) >> (Source o Args.src) ||
-  Args.$$$ "(" |-- Args.!!! (meth0 --| Args.$$$ ")")) x
-and meth3 x =
- (meth4 --| Args.$$$ "?" >> Try ||
-  meth4 --| Args.$$$ "+" >> Repeat1 ||
-  meth4 -- (Args.$$$ "[" |-- Scan.optional Args.nat 1 --| Args.$$$ "]") >> (SelectGoals o swap) ||
-  meth4) x
-and meth2 x =
- (Args.position (Args.name -- Args.generic_args1 is_symid_meth) >> (Source o Args.src) ||
-  meth3) x
-and meth1 x = (enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
-and meth0 x = (enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
-
-in val parse_args = meth3 end;
 
 
 (*final declarations of this structure!*)
 val unfold = unfold_meth;
 val fold = fold_meth;