unified Args.T with OuterLex.token, renamed some operations;
authorwenzelm
Sat Aug 09 22:43:46 2008 +0200 (2008-08-09)
changeset 27809a1e409db516b
parent 27808 4dd3d5efcc7f
child 27810 b09f6fcc1f3d
unified Args.T with OuterLex.token, renamed some operations;
doc-src/antiquote_setup.ML
src/FOL/ex/IffOracle.thy
src/HOL/Nominal/nominal_induct.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/split_rule.ML
src/Provers/blast.ML
src/Provers/clasimp.ML
src/Provers/eqsubst.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/rule_insts.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_thms.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_output.ML
src/Tools/code/code_target.ML
src/Tools/induct.ML
src/Tools/induct_tacs.ML
     1.1 --- a/doc-src/antiquote_setup.ML	Sat Aug 09 12:28:13 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Sat Aug 09 22:43:46 2008 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4    | clean_name "}" = "braceright"
     1.5    | clean_name s = s |> translate_string (fn "_" => "-" | c => c);
     1.6  
     1.7 -val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
     1.8 +val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src;
     1.9  
    1.10  fun tweak_line s =
    1.11    if ! O.display then s else Symbol.strip_blanks s;
     2.1 --- a/src/FOL/ex/IffOracle.thy	Sat Aug 09 12:28:13 2008 +0200
     2.2 +++ b/src/FOL/ex/IffOracle.thy	Sat Aug 09 22:43:46 2008 +0200
     2.3 @@ -53,7 +53,7 @@
     2.4  subsection {* Oracle as proof method *}
     2.5  
     2.6  method_setup iff = {*
     2.7 -  Method.simple_args Args.nat (fn n => fn ctxt =>
     2.8 +  Method.simple_args OuterParse.nat (fn n => fn ctxt =>
     2.9      Method.SIMPLE_METHOD
    2.10        (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt) n))
    2.11          handle Fail _ => no_tac))
     3.1 --- a/src/HOL/Nominal/nominal_induct.ML	Sat Aug 09 12:28:13 2008 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Sat Aug 09 22:43:46 2008 +0200
     3.3 @@ -123,6 +123,8 @@
     3.4  
     3.5  local
     3.6  
     3.7 +structure P = OuterParse;
     3.8 +
     3.9  val avoidingN = "avoiding";
    3.10  val fixingN = "arbitrary";  (* to be consistent with induct; hopefully this changes again *)
    3.11  val ruleN = "rule";
    3.12 @@ -145,7 +147,7 @@
    3.13    Scan.repeat (unless_more_args free)) [];
    3.14  
    3.15  val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
    3.16 -  Args.and_list (Scan.repeat (unless_more_args free))) [];
    3.17 +  P.and_list' (Scan.repeat (unless_more_args free))) [];
    3.18  
    3.19  val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms;
    3.20  
    3.21 @@ -153,7 +155,7 @@
    3.22  
    3.23  fun nominal_induct_method src =
    3.24    Method.syntax
    3.25 -   (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
    3.26 +   (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
    3.27      avoiding -- fixing -- rule_spec) src
    3.28    #> (fn ((((x, y), z), w), ctxt) =>
    3.29      Method.RAW_METHOD_CASES (fn facts =>
     4.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sat Aug 09 12:28:13 2008 +0200
     4.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sat Aug 09 22:43:46 2008 +0200
     4.3 @@ -697,6 +697,6 @@
     4.4  val setup =
     4.5    add_codegen "inductive" inductive_codegen #>
     4.6    Code.add_attribute ("ind", Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
     4.7 -    Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add);
     4.8 +    Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add);
     4.9  
    4.10  end;
     5.1 --- a/src/HOL/Tools/recdef_package.ML	Sat Aug 09 12:28:13 2008 +0200
     5.2 +++ b/src/HOL/Tools/recdef_package.ML	Sat Aug 09 22:43:46 2008 +0200
     5.3 @@ -295,7 +295,7 @@
     5.4  val _ = List.app OuterKeyword.keyword ["permissive", "congs", "hints"];
     5.5  
     5.6  val hints =
     5.7 -  P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;
     5.8 +  P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- Args.parse) --| P.$$$ ")") >> Args.src;
     5.9  
    5.10  val recdef_decl =
    5.11    Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
     6.1 --- a/src/HOL/Tools/res_axioms.ML	Sat Aug 09 12:28:13 2008 +0200
     6.2 +++ b/src/HOL/Tools/res_axioms.ML	Sat Aug 09 22:43:46 2008 +0200
     6.3 @@ -557,7 +557,7 @@
     6.4  
     6.5  (** Attribute for converting a theorem into clauses **)
     6.6  
     6.7 -val clausify = Attrib.syntax (Scan.lift Args.nat
     6.8 +val clausify = Attrib.syntax (Scan.lift OuterParse.nat
     6.9    >> (fn i => Thm.rule_attribute (fn context => fn th =>
    6.10        Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))));
    6.11  
     7.1 --- a/src/HOL/Tools/split_rule.ML	Sat Aug 09 12:28:13 2008 +0200
     7.2 +++ b/src/HOL/Tools/split_rule.ML	Sat Aug 09 22:43:46 2008 +0200
     7.3 @@ -146,12 +146,11 @@
     7.4  
     7.5  (* FIXME dynamically scoped due to Args.name/pair_tac *)
     7.6  
     7.7 -val split_format = Attrib.syntax
     7.8 -  (Scan.lift (Args.parens (Args.$$$ "complete"))
     7.9 -    >> K (Thm.rule_attribute (K complete_split_rule)) ||
    7.10 -  Args.and_list1 (Scan.lift (Scan.repeat Args.name))
    7.11 +val split_format = Attrib.syntax (Scan.lift
    7.12 + (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
    7.13 +  OuterParse.and_list1 (Scan.repeat Args.name)
    7.14      >> (fn xss => Thm.rule_attribute (fn context =>
    7.15 -        split_rule_goal (Context.proof_of context) xss)));
    7.16 +        split_rule_goal (Context.proof_of context) xss))));
    7.17  
    7.18  val setup =
    7.19    Attrib.add_attributes
     8.1 --- a/src/Provers/blast.ML	Sat Aug 09 12:28:13 2008 +0200
     8.2 +++ b/src/Provers/blast.ML	Sat Aug 09 22:43:46 2008 +0200
     8.3 @@ -1307,7 +1307,7 @@
     8.4  (** method setup **)
     8.5  
     8.6  val blast_method =
     8.7 -  Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option Args.nat))
     8.8 +  Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option OuterParse.nat))
     8.9      (fn NONE => Data.cla_meth' blast_tac
    8.10        | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim));
    8.11  
     9.1 --- a/src/Provers/clasimp.ML	Sat Aug 09 12:28:13 2008 +0200
     9.2 +++ b/src/Provers/clasimp.ML	Sat Aug 09 22:43:46 2008 +0200
     9.3 @@ -302,7 +302,8 @@
     9.4  
     9.5  
     9.6  fun auto_args m =
     9.7 -  Method.bang_sectioned_args' clasimp_modifiers (Scan.lift (Scan.option (Args.nat -- Args.nat))) m;
     9.8 +  Method.bang_sectioned_args' clasimp_modifiers
     9.9 +    (Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat))) m;
    9.10  
    9.11  fun auto_meth NONE = clasimp_meth (CHANGED_PROP o auto_tac)
    9.12    | auto_meth (SOME (m, n)) = clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n));
    10.1 --- a/src/Provers/eqsubst.ML	Sat Aug 09 12:28:13 2008 +0200
    10.2 +++ b/src/Provers/eqsubst.ML	Sat Aug 09 22:43:46 2008 +0200
    10.3 @@ -559,8 +559,7 @@
    10.4       (Scan.succeed false);
    10.5  
    10.6  val ith_syntax =
    10.7 -    (Args.parens (Scan.repeat Args.nat))
    10.8 -      || (Scan.succeed [0]);
    10.9 +    Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
   10.10  
   10.11  (* combination method that takes a flag (true indicates that subst
   10.12  should be done to an assumption, false = apply to the conclusion of
    11.1 --- a/src/Pure/Isar/context_rules.ML	Sat Aug 09 12:28:13 2008 +0200
    11.2 +++ b/src/Pure/Isar/context_rules.ML	Sat Aug 09 22:43:46 2008 +0200
    11.3 @@ -205,8 +205,8 @@
    11.4  (* concrete syntax *)
    11.5  
    11.6  fun add_args a b c = Attrib.syntax
    11.7 -  (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) -- Scan.option Args.nat)
    11.8 -    >> (fn (f, n) => f n));
    11.9 +  (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) --
   11.10 +    Scan.option OuterParse.nat) >> (fn (f, n) => f n));
   11.11  
   11.12  val rule_atts =
   11.13   [("intro", add_args intro_bang intro intro_query, "declaration of introduction rule"),
    12.1 --- a/src/Pure/Isar/rule_insts.ML	Sat Aug 09 12:28:13 2008 +0200
    12.2 +++ b/src/Pure/Isar/rule_insts.ML	Sat Aug 09 22:43:46 2008 +0200
    12.3 @@ -28,6 +28,9 @@
    12.4  structure RuleInsts: RULE_INSTS =
    12.5  struct
    12.6  
    12.7 +structure T = OuterLex;
    12.8 +structure P = OuterParse;
    12.9 +
   12.10  
   12.11  (** reading instantiations **)
   12.12  
   12.13 @@ -97,11 +100,11 @@
   12.14  
   12.15      val (type_insts, term_insts) = List.partition (is_tvar o fst) mixed_insts;
   12.16      val internal_insts = term_insts |> map_filter
   12.17 -      (fn (xi, Args.Term t) => SOME (xi, t)
   12.18 -        | (_, Args.Text _) => NONE
   12.19 +      (fn (xi, T.Term t) => SOME (xi, t)
   12.20 +        | (_, T.Text _) => NONE
   12.21          | (xi, _) => error_var "Term argument expected for " xi);
   12.22      val external_insts = term_insts |> map_filter
   12.23 -      (fn (xi, Args.Text s) => SOME (xi, s) | _ => NONE);
   12.24 +      (fn (xi, T.Text s) => SOME (xi, s) | _ => NONE);
   12.25  
   12.26  
   12.27      (* mixed type instantiations *)
   12.28 @@ -111,8 +114,8 @@
   12.29          val S = the_sort tvars xi;
   12.30          val T =
   12.31            (case arg of
   12.32 -            Args.Text s => Syntax.read_typ ctxt s
   12.33 -          | Args.Typ T => T
   12.34 +            T.Text s => Syntax.read_typ ctxt s
   12.35 +          | T.Typ T => T
   12.36            | _ => error_var "Type argument expected for " xi);
   12.37        in
   12.38          if Sign.of_sort thy (T, S) then ((xi, S), T)
   12.39 @@ -169,9 +172,9 @@
   12.40      val _ = (*assign internalized values*)
   12.41        mixed_insts |> List.app (fn (arg, (xi, _)) =>
   12.42          if is_tvar xi then
   12.43 -          Args.assign (SOME (Args.Typ (the (AList.lookup (op =) type_insts xi)))) arg
   12.44 +          T.assign (SOME (T.Typ (the (AList.lookup (op =) type_insts xi)))) arg
   12.45          else
   12.46 -          Args.assign (SOME (Args.Term (the (AList.lookup (op =) term_insts xi)))) arg);
   12.47 +          T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg);
   12.48    in
   12.49      Drule.instantiate insts thm |> RuleCases.save thm
   12.50    end;
   12.51 @@ -194,7 +197,7 @@
   12.52  
   12.53  fun read_instantiate ctxt args thm =
   12.54    read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic)  (* FIXME !? *)
   12.55 -    (map (fn (x, y) => (Args.eof, (x, Args.Text y))) args) thm;
   12.56 +    (map (fn (x, y) => (T.eof, (x, T.Text y))) args) thm;
   12.57  
   12.58  fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
   12.59  
   12.60 @@ -207,16 +210,16 @@
   12.61  local
   12.62  
   12.63  val value =
   12.64 -  Args.internal_typ >> Args.Typ ||
   12.65 -  Args.internal_term >> Args.Term ||
   12.66 -  Args.name >> Args.Text;
   12.67 +  Args.internal_typ >> T.Typ ||
   12.68 +  Args.internal_term >> T.Term ||
   12.69 +  Args.name >> T.Text;
   12.70  
   12.71 -val inst = Args.var -- (Args.$$$ "=" |-- Args.ahead -- value)
   12.72 +val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead P.not_eof -- value)
   12.73    >> (fn (xi, (a, v)) => (a, (xi, v)));
   12.74  
   12.75  in
   12.76  
   12.77 -val where_att = Attrib.syntax (Args.and_list (Scan.lift inst) >> (fn args =>
   12.78 +val where_att = Attrib.syntax (Scan.lift (P.and_list inst) >> (fn args =>
   12.79    Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)));
   12.80  
   12.81  end;
   12.82 @@ -227,10 +230,10 @@
   12.83  local
   12.84  
   12.85  val value =
   12.86 -  Args.internal_term >> Args.Term ||
   12.87 -  Args.name >> Args.Text;
   12.88 +  Args.internal_term >> T.Term ||
   12.89 +  Args.name >> T.Text;
   12.90  
   12.91 -val inst = Args.ahead -- Args.maybe value;
   12.92 +val inst = Scan.ahead P.not_eof -- Args.maybe value;
   12.93  val concl = Args.$$$ "concl" -- Args.colon;
   12.94  
   12.95  val insts =
   12.96 @@ -406,16 +409,16 @@
   12.97  
   12.98  val insts =
   12.99    Scan.optional
  12.100 -    (Args.and_list1 (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
  12.101 -      Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
  12.102 +    (Scan.lift (P.and_list1 (Args.name -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) []
  12.103 +    -- Attrib.thms;
  12.104  
  12.105  fun inst_args f src ctxt =
  12.106    f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
  12.107  
  12.108  val insts_var =
  12.109    Scan.optional
  12.110 -    (Args.and_list1 (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
  12.111 -      Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
  12.112 +    (Scan.lift (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) []
  12.113 +    -- Attrib.thms;
  12.114  
  12.115  fun inst_args_var f src ctxt =
  12.116    f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
    13.1 --- a/src/Pure/ML/ml_antiquote.ML	Sat Aug 09 12:28:13 2008 +0200
    13.2 +++ b/src/Pure/ML/ml_antiquote.ML	Sat Aug 09 22:43:46 2008 +0200
    13.3 @@ -62,6 +62,9 @@
    13.4  
    13.5  (** concrete antiquotations **)
    13.6  
    13.7 +structure P = OuterParse;
    13.8 +
    13.9 +
   13.10  (* misc *)
   13.11  
   13.12  val _ = value "theory"
   13.13 @@ -83,11 +86,11 @@
   13.14  val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
   13.15  
   13.16  val _ = macro "let" (Args.context --
   13.17 -  Args.and_list1 (Args.and_list1 (Scan.lift Args.name) -- Scan.lift (Args.$$$ "=" |-- Args.name))
   13.18 +  Scan.lift (P.and_list1 (P.and_list1 Args.name -- (Args.$$$ "=" |-- Args.name)))
   13.19      >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
   13.20  
   13.21  val _ = macro "note" (Args.context :|-- (fn ctxt =>
   13.22 -  Args.and_list1 (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
   13.23 +  P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
   13.24      ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
   13.25    >> (fn args => #2 (ProofContext.note_thmss_i "" args ctxt))));
   13.26  
   13.27 @@ -123,8 +126,8 @@
   13.28  val _ = inline "const_syntax" (const true);
   13.29  
   13.30  val _ = inline "const"
   13.31 -  (Args.context -- Scan.lift Args.name --
   13.32 -    Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   13.33 +  (Args.context -- Scan.lift Args.name -- Scan.optional
   13.34 +      (Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   13.35      >> (fn ((ctxt, c), Ts) =>
   13.36        let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
   13.37        in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));
    14.1 --- a/src/Pure/ML/ml_context.ML	Sat Aug 09 12:28:13 2008 +0200
    14.2 +++ b/src/Pure/ML/ml_context.ML	Sat Aug 09 22:43:46 2008 +0200
    14.3 @@ -118,7 +118,7 @@
    14.4  structure P = OuterParse;
    14.5  
    14.6  val antiq =
    14.7 -  P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof)
    14.8 +  P.!!! (P.position P.xname -- Args.parse --| Scan.ahead P.eof)
    14.9    >> (fn ((x, pos), y) => Args.src ((x, y), pos));
   14.10  
   14.11  fun eval_antiquotes struct_name (txt, pos) opt_ctxt =
    15.1 --- a/src/Pure/ML/ml_thms.ML	Sat Aug 09 12:28:13 2008 +0200
    15.2 +++ b/src/Pure/ML/ml_thms.ML	Sat Aug 09 22:43:46 2008 +0200
    15.3 @@ -49,12 +49,12 @@
    15.4  
    15.5  (* ad-hoc goals *)
    15.6  
    15.7 -fun by x = Scan.lift (Args.$$$ "by") x;
    15.8 -val goal = Scan.unless by Args.prop;
    15.9 +val by = Args.$$$ "by";
   15.10 +val goal = Scan.unless (Scan.lift by) Args.prop;
   15.11  
   15.12  val _ = ML_Context.add_antiq "lemma"
   15.13 -  ((Args.context -- Args.mode "open" -- Scan.repeat1 goal --
   15.14 -      (by |-- Scan.lift Method.parse_args -- Scan.option (Scan.lift Method.parse_args))) >>
   15.15 +  (Args.context -- Args.mode "open" -- Scan.repeat1 goal --
   15.16 +      Scan.lift (by |-- Method.parse -- Scan.option Method.parse) >>
   15.17      (fn (((ctxt, is_open), props), methods) => fn {struct_name, background} =>
   15.18        let
   15.19          val i = serial ();
    16.1 --- a/src/Pure/Thy/latex.ML	Sat Aug 09 12:28:13 2008 +0200
    16.2 +++ b/src/Pure/Thy/latex.ML	Sat Aug 09 22:43:46 2008 +0200
    16.3 @@ -107,7 +107,7 @@
    16.4  val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
    16.5  
    16.6  fun output_basic tok =
    16.7 -  let val s = T.val_of tok in
    16.8 +  let val s = T.content_of tok in
    16.9      if invisible_token tok then ""
   16.10      else if T.is_kind T.Command tok then
   16.11        "\\isacommand{" ^ output_syms s ^ "}"
    17.1 --- a/src/Pure/Thy/thy_output.ML	Sat Aug 09 12:28:13 2008 +0200
    17.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Aug 09 22:43:46 2008 +0200
    17.3 @@ -135,7 +135,7 @@
    17.4  
    17.5  in
    17.6  
    17.7 -val antiq = P.!!! (P.position P.xname -- properties -- P.arguments --| Scan.ahead P.eof)
    17.8 +val antiq = P.!!! (P.position P.xname -- properties -- Args.parse --| Scan.ahead P.eof)
    17.9    >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
   17.10  
   17.11  end;
   17.12 @@ -332,18 +332,18 @@
   17.13        >> (fn d => (NONE, (NoToken, ("", d))));
   17.14  
   17.15      fun markup mark mk flag = Scan.peek (fn d =>
   17.16 -      improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.val_of)) --
   17.17 +      improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
   17.18        Scan.repeat tag --
   17.19        P.!!!! ((improper -- locale -- improper) |-- P.position P.text --| improper_end)
   17.20        >> (fn (((tok, pos), tags), txt) =>
   17.21 -        let val name = T.val_of tok
   17.22 +        let val name = T.content_of tok
   17.23          in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
   17.24  
   17.25      val command = Scan.peek (fn d =>
   17.26        P.position (Scan.one (T.is_kind T.Command)) --
   17.27        Scan.repeat tag
   17.28        >> (fn ((tok, pos), tags) =>
   17.29 -        let val name = T.val_of tok
   17.30 +        let val name = T.content_of tok
   17.31          in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
   17.32  
   17.33      val cmt = Scan.peek (fn d =>
   17.34 @@ -428,7 +428,7 @@
   17.35  
   17.36  (* basic pretty printing *)
   17.37  
   17.38 -val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
   17.39 +val str_of_source = space_implode " " o map T.unparse o #2 o #1 o Args.dest_src;
   17.40  
   17.41  fun tweak_line s =
   17.42    if ! display then s else Symbol.strip_blanks s;
   17.43 @@ -527,7 +527,7 @@
   17.44    in pretty_term ctxt prop end;
   17.45  
   17.46  val embedded_lemma =
   17.47 -  args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse_args -- Scan.option Method.parse_args))
   17.48 +  args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
   17.49      (output pretty_lemma o (fn ((a, arg :: _), p) => (Args.src ((a, [arg]), p))) o Args.dest_src);
   17.50  
   17.51  
   17.52 @@ -553,8 +553,8 @@
   17.53    ("prf", args Attrib.thms (output (pretty_prf false))),
   17.54    ("full_prf", args Attrib.thms (output (pretty_prf true))),
   17.55    ("theory", args (Scan.lift Args.name) (output pretty_theory)),
   17.56 -  ("ML", args (Scan.lift (Args.position Args.name)) (output_ml ml_val)),
   17.57 -  ("ML_type", args (Scan.lift (Args.position Args.name)) (output_ml ml_type)),
   17.58 -  ("ML_struct", args (Scan.lift (Args.position Args.name)) (output_ml ml_struct))];
   17.59 +  ("ML", args (Scan.lift (P.position Args.name)) (output_ml ml_val)),
   17.60 +  ("ML_type", args (Scan.lift (P.position Args.name)) (output_ml ml_type)),
   17.61 +  ("ML_struct", args (Scan.lift (P.position Args.name)) (output_ml ml_struct))];
   17.62  
   17.63  end;
    18.1 --- a/src/Tools/code/code_target.ML	Sat Aug 09 12:28:13 2008 +0200
    18.2 +++ b/src/Tools/code/code_target.ML	Sat Aug 09 22:43:46 2008 +0200
    18.3 @@ -318,7 +318,7 @@
    18.4  fun serialize thy = mount_serializer thy NONE;
    18.5  
    18.6  fun parse_args f args =
    18.7 -  case Scan.read Args.stopper f args
    18.8 +  case Scan.read OuterLex.stopper f args
    18.9     of SOME x => x
   18.10      | NONE => error "Bad serializer arguments";
   18.11  
   18.12 @@ -2243,7 +2243,7 @@
   18.13    -- Scan.repeat (P.$$$ inK |-- P.name
   18.14       -- Scan.option (P.$$$ module_nameK |-- P.name)
   18.15       -- Scan.option (P.$$$ fileK |-- P.name)
   18.16 -     -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
   18.17 +     -- Scan.optional (P.$$$ "(" |-- Args.parse --| P.$$$ ")") []
   18.18    ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
   18.19  
   18.20  val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK, inK, module_nameK, fileK];
    19.1 --- a/src/Tools/induct.ML	Sat Aug 09 12:28:13 2008 +0200
    19.2 +++ b/src/Tools/induct.ML	Sat Aug 09 22:43:46 2008 +0200
    19.3 @@ -686,6 +686,8 @@
    19.4  
    19.5  (** concrete syntax **)
    19.6  
    19.7 +structure P = OuterParse;
    19.8 +
    19.9  val arbitraryN = "arbitrary";
   19.10  val takingN = "taking";
   19.11  val ruleN = "rule";
   19.12 @@ -726,7 +728,7 @@
   19.13      Args.$$$ predN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
   19.14  
   19.15  val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
   19.16 -  Args.and_list1 (Scan.repeat (unless_more_args free))) [];
   19.17 +  P.and_list1' (Scan.repeat (unless_more_args free))) [];
   19.18  
   19.19  val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
   19.20    Scan.repeat1 (unless_more_args inst)) [];
   19.21 @@ -734,13 +736,13 @@
   19.22  in
   19.23  
   19.24  fun cases_meth src =
   19.25 -  Method.syntax (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) src
   19.26 +  Method.syntax (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) src
   19.27    #> (fn ((insts, opt_rule), ctxt) =>
   19.28      Method.METHOD_CASES (fn facts =>
   19.29        Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
   19.30  
   19.31  fun induct_meth src =
   19.32 -  Method.syntax (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
   19.33 +  Method.syntax (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
   19.34      (arbitrary -- taking -- Scan.option induct_rule)) src
   19.35    #> (fn ((insts, ((arbitrary, taking), opt_rule)), ctxt) =>
   19.36      Method.RAW_METHOD_CASES (fn facts =>
    20.1 --- a/src/Tools/induct_tacs.ML	Sat Aug 09 12:28:13 2008 +0200
    20.2 +++ b/src/Tools/induct_tacs.ML	Sat Aug 09 22:43:46 2008 +0200
    20.3 @@ -117,7 +117,7 @@
    20.4  val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
    20.5  
    20.6  val varss =
    20.7 -  Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
    20.8 +  OuterParse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
    20.9  
   20.10  in
   20.11