changeset 27809 | a1e409db516b |
parent 27033 | 6ef5134fc631 |
child 29269 | 5c25a2012975 |
--- 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