src/Tools/eqsubst.ML
changeset 53168 d998de7f0efc
parent 52732 b4da1f2ec73f
child 54742 7a86358a3c0b
     1.1 --- a/src/Tools/eqsubst.ML	Fri Aug 23 15:36:54 2013 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Fri Aug 23 17:01:12 2013 +0200
     1.3 @@ -420,7 +420,7 @@
     1.4     the goal) as well as the theorems to use *)
     1.5  val setup =
     1.6    Method.setup @{binding subst}
     1.7 -    (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
     1.8 +    (Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
     1.9          Attrib.thms >>
    1.10        (fn ((asm, occs), inthms) => fn ctxt =>
    1.11          SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))