src/Provers/eqsubst.ML
changeset 27809 a1e409db516b
parent 27033 6ef5134fc631
child 29269 5c25a2012975
     1.1 --- a/src/Provers/eqsubst.ML	Sat Aug 09 12:28:13 2008 +0200
     1.2 +++ b/src/Provers/eqsubst.ML	Sat Aug 09 22:43:46 2008 +0200
     1.3 @@ -559,8 +559,7 @@
     1.4       (Scan.succeed false);
     1.5  
     1.6  val ith_syntax =
     1.7 -    (Args.parens (Scan.repeat Args.nat))
     1.8 -      || (Scan.succeed [0]);
     1.9 +    Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
    1.10  
    1.11  (* combination method that takes a flag (true indicates that subst
    1.12  should be done to an assumption, false = apply to the conclusion of