1.1 --- a/src/Tools/eqsubst.ML	Tue Aug 09 15:41:00 2011 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Tue Aug 09 15:50:13 2011 +0200
     1.3 @@ -108,10 +108,6 @@
     1.4      val searchf_bt_unify_valid :
     1.5         searchinfo -> term -> match Seq.seq Seq.seq
     1.6  
     1.7 -    (* syntax tools *)
     1.8 -    val ith_syntax : int list parser
     1.9 -    val options_syntax : bool parser
    1.10 -
    1.11      (* Isar level hooks *)
    1.12      val eqsubst_asm_meth : Proof.context -> int list -> thm list -> Proof.method
    1.13      val eqsubst_meth : Proof.context -> int list -> thm list -> Proof.method
    1.14 @@ -546,23 +542,15 @@
    1.15  fun eqsubst_asm_meth ctxt occL inthms =
    1.16      SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
    1.17  
    1.18 -(* syntax for options, given "(asm)" will give back true, without
    1.19 -   gives back false *)
    1.20 -val options_syntax =
    1.21 -    (Args.parens (Args.$$$ "asm") >> (K true)) ||
    1.22 -     (Scan.succeed false);
    1.23 -
    1.24 -val ith_syntax =
    1.25 -    Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0];
    1.26 -
    1.27  (* combination method that takes a flag (true indicates that subst
    1.28     should be done to an assumption, false = apply to the conclusion of
    1.29     the goal) as well as the theorems to use *)
    1.30  val setup =
    1.31    Method.setup @{binding subst}
    1.32 -    (Scan.lift (options_syntax -- ith_syntax) -- Attrib.thms >>
    1.33 -      (fn ((asmflag, occL), inthms) => fn ctxt =>
    1.34 -        (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
    1.35 +    (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
    1.36 +        Attrib.thms >>
    1.37 +      (fn ((asm, occL), inthms) => fn ctxt =>
    1.38 +        (if asm then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
    1.39      "single-step substitution";
    1.40  
    1.41  end;