# HG changeset patch
# User wenzelm
# Date 1218314626 -7200
# Node ID a1e409db516be29993314760d06215def7133cc6
# Parent  4dd3d5efcc7f73f0e815bf4e4fe302e754226921
unified Args.T with OuterLex.token, renamed some operations;

diff -r 4dd3d5efcc7f -r a1e409db516b doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/doc-src/antiquote_setup.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -30,7 +30,7 @@
   | clean_name "}" = "braceright"
   | clean_name s = s |> translate_string (fn "_" => "-" | c => c);
 
-val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
+val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src;
 
 fun tweak_line s =
   if ! O.display then s else Symbol.strip_blanks s;
diff -r 4dd3d5efcc7f -r a1e409db516b src/FOL/ex/IffOracle.thy
--- a/src/FOL/ex/IffOracle.thy	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/FOL/ex/IffOracle.thy	Sat Aug 09 22:43:46 2008 +0200
@@ -53,7 +53,7 @@
 subsection {* Oracle as proof method *}
 
 method_setup iff = {*
-  Method.simple_args Args.nat (fn n => fn ctxt =>
+  Method.simple_args OuterParse.nat (fn n => fn ctxt =>
     Method.SIMPLE_METHOD
       (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt) n))
         handle Fail _ => no_tac))
diff -r 4dd3d5efcc7f -r a1e409db516b src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -123,6 +123,8 @@
 
 local
 
+structure P = OuterParse;
+
 val avoidingN = "avoiding";
 val fixingN = "arbitrary";  (* to be consistent with induct; hopefully this changes again *)
 val ruleN = "rule";
@@ -145,7 +147,7 @@
   Scan.repeat (unless_more_args free)) [];
 
 val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
-  Args.and_list (Scan.repeat (unless_more_args free))) [];
+  P.and_list' (Scan.repeat (unless_more_args free))) [];
 
 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms;
 
@@ -153,7 +155,7 @@
 
 fun nominal_induct_method src =
   Method.syntax
-   (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
+   (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
     avoiding -- fixing -- rule_spec) src
   #> (fn ((((x, y), z), w), ctxt) =>
     Method.RAW_METHOD_CASES (fn facts =>
diff -r 4dd3d5efcc7f -r a1e409db516b src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -697,6 +697,6 @@
 val setup =
   add_codegen "inductive" inductive_codegen #>
   Code.add_attribute ("ind", Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
-    Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add);
+    Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add);
 
 end;
diff -r 4dd3d5efcc7f -r a1e409db516b src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -295,7 +295,7 @@
 val _ = List.app OuterKeyword.keyword ["permissive", "congs", "hints"];
 
 val hints =
-  P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;
+  P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- Args.parse) --| P.$$$ ")") >> Args.src;
 
 val recdef_decl =
   Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
diff -r 4dd3d5efcc7f -r a1e409db516b src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -557,7 +557,7 @@
 
 (** Attribute for converting a theorem into clauses **)
 
-val clausify = Attrib.syntax (Scan.lift Args.nat
+val clausify = Attrib.syntax (Scan.lift OuterParse.nat
   >> (fn i => Thm.rule_attribute (fn context => fn th =>
       Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))));
 
diff -r 4dd3d5efcc7f -r a1e409db516b src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/HOL/Tools/split_rule.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -146,12 +146,11 @@
 
 (* FIXME dynamically scoped due to Args.name/pair_tac *)
 
-val split_format = Attrib.syntax
-  (Scan.lift (Args.parens (Args.$$$ "complete"))
-    >> K (Thm.rule_attribute (K complete_split_rule)) ||
-  Args.and_list1 (Scan.lift (Scan.repeat Args.name))
+val split_format = Attrib.syntax (Scan.lift
+ (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
+  OuterParse.and_list1 (Scan.repeat Args.name)
     >> (fn xss => Thm.rule_attribute (fn context =>
-        split_rule_goal (Context.proof_of context) xss)));
+        split_rule_goal (Context.proof_of context) xss))));
 
 val setup =
   Attrib.add_attributes
diff -r 4dd3d5efcc7f -r a1e409db516b src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Provers/blast.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -1307,7 +1307,7 @@
 (** method setup **)
 
 val blast_method =
-  Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option Args.nat))
+  Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option OuterParse.nat))
     (fn NONE => Data.cla_meth' blast_tac
       | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim));
 
diff -r 4dd3d5efcc7f -r a1e409db516b src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Provers/clasimp.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -302,7 +302,8 @@
 
 
 fun auto_args m =
-  Method.bang_sectioned_args' clasimp_modifiers (Scan.lift (Scan.option (Args.nat -- Args.nat))) m;
+  Method.bang_sectioned_args' clasimp_modifiers
+    (Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat))) m;
 
 fun auto_meth NONE = clasimp_meth (CHANGED_PROP o auto_tac)
   | auto_meth (SOME (m, n)) = clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n));
diff -r 4dd3d5efcc7f -r a1e409db516b src/Provers/eqsubst.ML
--- a/src/Provers/eqsubst.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Provers/eqsubst.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -559,8 +559,7 @@
      (Scan.succeed false);
 
 val ith_syntax =
-    (Args.parens (Scan.repeat Args.nat))
-      || (Scan.succeed [0]);
+    Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
 
 (* combination method that takes a flag (true indicates that subst
 should be done to an assumption, false = apply to the conclusion of
diff -r 4dd3d5efcc7f -r a1e409db516b src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Pure/Isar/context_rules.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -205,8 +205,8 @@
 (* concrete syntax *)
 
 fun add_args a b c = Attrib.syntax
-  (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) -- Scan.option Args.nat)
-    >> (fn (f, n) => f n));
+  (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) --
+    Scan.option OuterParse.nat) >> (fn (f, n) => f n));
 
 val rule_atts =
  [("intro", add_args intro_bang intro intro_query, "declaration of introduction rule"),
diff -r 4dd3d5efcc7f -r a1e409db516b src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -28,6 +28,9 @@
 structure RuleInsts: RULE_INSTS =
 struct
 
+structure T = OuterLex;
+structure P = OuterParse;
+
 
 (** reading instantiations **)
 
@@ -97,11 +100,11 @@
 
     val (type_insts, term_insts) = List.partition (is_tvar o fst) mixed_insts;
     val internal_insts = term_insts |> map_filter
-      (fn (xi, Args.Term t) => SOME (xi, t)
-        | (_, Args.Text _) => NONE
+      (fn (xi, T.Term t) => SOME (xi, t)
+        | (_, T.Text _) => NONE
         | (xi, _) => error_var "Term argument expected for " xi);
     val external_insts = term_insts |> map_filter
-      (fn (xi, Args.Text s) => SOME (xi, s) | _ => NONE);
+      (fn (xi, T.Text s) => SOME (xi, s) | _ => NONE);
 
 
     (* mixed type instantiations *)
@@ -111,8 +114,8 @@
         val S = the_sort tvars xi;
         val T =
           (case arg of
-            Args.Text s => Syntax.read_typ ctxt s
-          | Args.Typ T => T
+            T.Text s => Syntax.read_typ ctxt s
+          | T.Typ T => T
           | _ => error_var "Type argument expected for " xi);
       in
         if Sign.of_sort thy (T, S) then ((xi, S), T)
@@ -169,9 +172,9 @@
     val _ = (*assign internalized values*)
       mixed_insts |> List.app (fn (arg, (xi, _)) =>
         if is_tvar xi then
-          Args.assign (SOME (Args.Typ (the (AList.lookup (op =) type_insts xi)))) arg
+          T.assign (SOME (T.Typ (the (AList.lookup (op =) type_insts xi)))) arg
         else
-          Args.assign (SOME (Args.Term (the (AList.lookup (op =) term_insts xi)))) arg);
+          T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg);
   in
     Drule.instantiate insts thm |> RuleCases.save thm
   end;
@@ -194,7 +197,7 @@
 
 fun read_instantiate ctxt args thm =
   read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic)  (* FIXME !? *)
-    (map (fn (x, y) => (Args.eof, (x, Args.Text y))) args) thm;
+    (map (fn (x, y) => (T.eof, (x, T.Text y))) args) thm;
 
 fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
 
@@ -207,16 +210,16 @@
 local
 
 val value =
-  Args.internal_typ >> Args.Typ ||
-  Args.internal_term >> Args.Term ||
-  Args.name >> Args.Text;
+  Args.internal_typ >> T.Typ ||
+  Args.internal_term >> T.Term ||
+  Args.name >> T.Text;
 
-val inst = Args.var -- (Args.$$$ "=" |-- Args.ahead -- value)
+val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead P.not_eof -- value)
   >> (fn (xi, (a, v)) => (a, (xi, v)));
 
 in
 
-val where_att = Attrib.syntax (Args.and_list (Scan.lift inst) >> (fn args =>
+val where_att = Attrib.syntax (Scan.lift (P.and_list inst) >> (fn args =>
   Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)));
 
 end;
@@ -227,10 +230,10 @@
 local
 
 val value =
-  Args.internal_term >> Args.Term ||
-  Args.name >> Args.Text;
+  Args.internal_term >> T.Term ||
+  Args.name >> T.Text;
 
-val inst = Args.ahead -- Args.maybe value;
+val inst = Scan.ahead P.not_eof -- Args.maybe value;
 val concl = Args.$$$ "concl" -- Args.colon;
 
 val insts =
@@ -406,16 +409,16 @@
 
 val insts =
   Scan.optional
-    (Args.and_list1 (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
-      Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
+    (Scan.lift (P.and_list1 (Args.name -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) []
+    -- Attrib.thms;
 
 fun inst_args f src ctxt =
   f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
 
 val insts_var =
   Scan.optional
-    (Args.and_list1 (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
-      Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
+    (Scan.lift (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) []
+    -- Attrib.thms;
 
 fun inst_args_var f src ctxt =
   f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
diff -r 4dd3d5efcc7f -r a1e409db516b src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -62,6 +62,9 @@
 
 (** concrete antiquotations **)
 
+structure P = OuterParse;
+
+
 (* misc *)
 
 val _ = value "theory"
@@ -83,11 +86,11 @@
 val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
 
 val _ = macro "let" (Args.context --
-  Args.and_list1 (Args.and_list1 (Scan.lift Args.name) -- Scan.lift (Args.$$$ "=" |-- Args.name))
+  Scan.lift (P.and_list1 (P.and_list1 Args.name -- (Args.$$$ "=" |-- Args.name)))
     >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
 
 val _ = macro "note" (Args.context :|-- (fn ctxt =>
-  Args.and_list1 (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
+  P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
     ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
   >> (fn args => #2 (ProofContext.note_thmss_i "" args ctxt))));
 
@@ -123,8 +126,8 @@
 val _ = inline "const_syntax" (const true);
 
 val _ = inline "const"
-  (Args.context -- Scan.lift Args.name --
-    Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) []
+  (Args.context -- Scan.lift Args.name -- Scan.optional
+      (Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
     >> (fn ((ctxt, c), Ts) =>
       let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
       in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));
diff -r 4dd3d5efcc7f -r a1e409db516b src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Pure/ML/ml_context.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -118,7 +118,7 @@
 structure P = OuterParse;
 
 val antiq =
-  P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof)
+  P.!!! (P.position P.xname -- Args.parse --| Scan.ahead P.eof)
   >> (fn ((x, pos), y) => Args.src ((x, y), pos));
 
 fun eval_antiquotes struct_name (txt, pos) opt_ctxt =
diff -r 4dd3d5efcc7f -r a1e409db516b src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Pure/ML/ml_thms.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -49,12 +49,12 @@
 
 (* ad-hoc goals *)
 
-fun by x = Scan.lift (Args.$$$ "by") x;
-val goal = Scan.unless by Args.prop;
+val by = Args.$$$ "by";
+val goal = Scan.unless (Scan.lift by) Args.prop;
 
 val _ = ML_Context.add_antiq "lemma"
-  ((Args.context -- Args.mode "open" -- Scan.repeat1 goal --
-      (by |-- Scan.lift Method.parse_args -- Scan.option (Scan.lift Method.parse_args))) >>
+  (Args.context -- Args.mode "open" -- Scan.repeat1 goal --
+      Scan.lift (by |-- Method.parse -- Scan.option Method.parse) >>
     (fn (((ctxt, is_open), props), methods) => fn {struct_name, background} =>
       let
         val i = serial ();
diff -r 4dd3d5efcc7f -r a1e409db516b src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Pure/Thy/latex.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -107,7 +107,7 @@
 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
 
 fun output_basic tok =
-  let val s = T.val_of tok in
+  let val s = T.content_of tok in
     if invisible_token tok then ""
     else if T.is_kind T.Command tok then
       "\\isacommand{" ^ output_syms s ^ "}"
diff -r 4dd3d5efcc7f -r a1e409db516b src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -135,7 +135,7 @@
 
 in
 
-val antiq = P.!!! (P.position P.xname -- properties -- P.arguments --| Scan.ahead P.eof)
+val antiq = P.!!! (P.position P.xname -- properties -- Args.parse --| Scan.ahead P.eof)
   >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
 
 end;
@@ -332,18 +332,18 @@
       >> (fn d => (NONE, (NoToken, ("", d))));
 
     fun markup mark mk flag = Scan.peek (fn d =>
-      improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.val_of)) --
+      improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
       Scan.repeat tag --
       P.!!!! ((improper -- locale -- improper) |-- P.position P.text --| improper_end)
       >> (fn (((tok, pos), tags), txt) =>
-        let val name = T.val_of tok
+        let val name = T.content_of tok
         in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
 
     val command = Scan.peek (fn d =>
       P.position (Scan.one (T.is_kind T.Command)) --
       Scan.repeat tag
       >> (fn ((tok, pos), tags) =>
-        let val name = T.val_of tok
+        let val name = T.content_of tok
         in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
 
     val cmt = Scan.peek (fn d =>
@@ -428,7 +428,7 @@
 
 (* basic pretty printing *)
 
-val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
+val str_of_source = space_implode " " o map T.unparse o #2 o #1 o Args.dest_src;
 
 fun tweak_line s =
   if ! display then s else Symbol.strip_blanks s;
@@ -527,7 +527,7 @@
   in pretty_term ctxt prop end;
 
 val embedded_lemma =
-  args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse_args -- Scan.option Method.parse_args))
+  args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
     (output pretty_lemma o (fn ((a, arg :: _), p) => (Args.src ((a, [arg]), p))) o Args.dest_src);
 
 
@@ -553,8 +553,8 @@
   ("prf", args Attrib.thms (output (pretty_prf false))),
   ("full_prf", args Attrib.thms (output (pretty_prf true))),
   ("theory", args (Scan.lift Args.name) (output pretty_theory)),
-  ("ML", args (Scan.lift (Args.position Args.name)) (output_ml ml_val)),
-  ("ML_type", args (Scan.lift (Args.position Args.name)) (output_ml ml_type)),
-  ("ML_struct", args (Scan.lift (Args.position Args.name)) (output_ml ml_struct))];
+  ("ML", args (Scan.lift (P.position Args.name)) (output_ml ml_val)),
+  ("ML_type", args (Scan.lift (P.position Args.name)) (output_ml ml_type)),
+  ("ML_struct", args (Scan.lift (P.position Args.name)) (output_ml ml_struct))];
 
 end;
diff -r 4dd3d5efcc7f -r a1e409db516b src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Tools/code/code_target.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -318,7 +318,7 @@
 fun serialize thy = mount_serializer thy NONE;
 
 fun parse_args f args =
-  case Scan.read Args.stopper f args
+  case Scan.read OuterLex.stopper f args
    of SOME x => x
     | NONE => error "Bad serializer arguments";
 
@@ -2243,7 +2243,7 @@
   -- Scan.repeat (P.$$$ inK |-- P.name
      -- Scan.option (P.$$$ module_nameK |-- P.name)
      -- Scan.option (P.$$$ fileK |-- P.name)
-     -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
+     -- Scan.optional (P.$$$ "(" |-- Args.parse --| P.$$$ ")") []
   ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
 
 val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK, inK, module_nameK, fileK];
diff -r 4dd3d5efcc7f -r a1e409db516b src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Tools/induct.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -686,6 +686,8 @@
 
 (** concrete syntax **)
 
+structure P = OuterParse;
+
 val arbitraryN = "arbitrary";
 val takingN = "taking";
 val ruleN = "rule";
@@ -726,7 +728,7 @@
     Args.$$$ predN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
 
 val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
-  Args.and_list1 (Scan.repeat (unless_more_args free))) [];
+  P.and_list1' (Scan.repeat (unless_more_args free))) [];
 
 val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
   Scan.repeat1 (unless_more_args inst)) [];
@@ -734,13 +736,13 @@
 in
 
 fun cases_meth src =
-  Method.syntax (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) src
+  Method.syntax (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) src
   #> (fn ((insts, opt_rule), ctxt) =>
     Method.METHOD_CASES (fn facts =>
       Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
 
 fun induct_meth src =
-  Method.syntax (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
+  Method.syntax (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
     (arbitrary -- taking -- Scan.option induct_rule)) src
   #> (fn ((insts, ((arbitrary, taking), opt_rule)), ctxt) =>
     Method.RAW_METHOD_CASES (fn facts =>
diff -r 4dd3d5efcc7f -r a1e409db516b src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Tools/induct_tacs.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -117,7 +117,7 @@
 val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
 
 val varss =
-  Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
+  OuterParse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
 
 in