src/Tools/eqsubst.ML
changeset 36970 01594f816e3a
parent 33259 17014b1b9353
child 40978 441260986b63
     1.1 --- a/src/Tools/eqsubst.ML	Mon May 17 15:11:25 2010 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Mon May 17 23:54:15 2010 +0200
     1.3 @@ -556,7 +556,7 @@
     1.4       (Scan.succeed false);
     1.5  
     1.6  val ith_syntax =
     1.7 -    Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
     1.8 +    Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0];
     1.9  
    1.10  (* combination method that takes a flag (true indicates that subst
    1.11     should be done to an assumption, false = apply to the conclusion of