1.1 --- a/src/Pure/Isar/method.ML	Sat May 15 22:24:25 2010 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Sat May 15 23:16:32 2010 +0200
     1.3 @@ -382,9 +382,6 @@
     1.4  
     1.5  (** concrete syntax **)
     1.6  
     1.7 -structure P = OuterParse;
     1.8 -
     1.9 -
    1.10  (* sections *)
    1.11  
    1.12  type modifier = (Proof.context -> Proof.context) * attribute;
    1.13 @@ -407,7 +404,7 @@
    1.14  (* extra rule methods *)
    1.15  
    1.16  fun xrule_meth m =
    1.17 -  Scan.lift (Scan.optional (Args.parens OuterParse.nat) 0) -- Attrib.thms >>
    1.18 +  Scan.lift (Scan.optional (Args.parens Parse.nat) 0) -- Attrib.thms >>
    1.19    (fn (n, ths) => K (m n ths));
    1.20  
    1.21  
    1.22 @@ -419,18 +416,18 @@
    1.23  local
    1.24  
    1.25  fun meth4 x =
    1.26 - (P.position (P.xname >> rpair []) >> (Source o Args.src) ||
    1.27 -  P.$$$ "(" |-- P.!!! (meth0 --| P.$$$ ")")) x
    1.28 + (Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) ||
    1.29 +  Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
    1.30  and meth3 x =
    1.31 - (meth4 --| P.$$$ "?" >> Try ||
    1.32 -  meth4 --| P.$$$ "+" >> Repeat1 ||
    1.33 -  meth4 -- (P.$$$ "[" |-- Scan.optional P.nat 1 --| P.$$$ "]") >> (SelectGoals o swap) ||
    1.34 + (meth4 --| Parse.$$$ "?" >> Try ||
    1.35 +  meth4 --| Parse.$$$ "+" >> Repeat1 ||
    1.36 +  meth4 -- (Parse.$$$ "[" |-- Scan.optional Parse.nat 1 --| Parse.$$$ "]") >> (SelectGoals o swap) ||
    1.37    meth4) x
    1.38  and meth2 x =
    1.39 - (P.position (P.xname -- Args.parse1 is_symid_meth) >> (Source o Args.src) ||
    1.40 + (Parse.position (Parse.xname -- Args.parse1 is_symid_meth) >> (Source o Args.src) ||
    1.41    meth3) x
    1.42 -and meth1 x = (P.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
    1.43 -and meth0 x = (P.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
    1.44 +and meth1 x = (Parse.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
    1.45 +and meth0 x = (Parse.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
    1.46  
    1.47  in val parse = meth3 end;
    1.48  
    1.49 @@ -463,12 +460,12 @@
    1.50    setup (Binding.name "rename_tac") (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
    1.51      (fn (quant, xs) => K (SIMPLE_METHOD'' quant (Tactic.rename_tac xs))))
    1.52      "rename parameters of goal" #>
    1.53 -  setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional P.int 1) >>
    1.54 +  setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
    1.55      (fn (quant, i) => K (SIMPLE_METHOD'' quant (Tactic.rotate_tac i))))
    1.56        "rotate assumptions of goal" #>
    1.57 -  setup (Binding.name "tactic") (Scan.lift (P.position Args.name) >> tactic)
    1.58 +  setup (Binding.name "tactic") (Scan.lift (Parse.position Args.name) >> tactic)
    1.59      "ML tactic as proof method" #>
    1.60 -  setup (Binding.name "raw_tactic") (Scan.lift (P.position Args.name) >> raw_tactic)
    1.61 +  setup (Binding.name "raw_tactic") (Scan.lift (Parse.position Args.name) >> raw_tactic)
    1.62      "ML tactic as raw proof method"));
    1.63  
    1.64