1.1 --- a/src/HOL/Integ/presburger.ML Sun Jun 06 18:35:39 2004 +0200
1.2 +++ b/src/HOL/Integ/presburger.ML Sun Jun 06 18:36:36 2004 +0200
1.3 @@ -282,7 +282,7 @@
1.4 || Args.$$$ "abs" >> K (apsnd (K true));
1.5 in
1.6 Method.simple_args
1.7 - (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >>
1.8 + (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
1.9 curry (foldl op |>) (true, false))
1.10 (fn (q,a) => fn _ => meth q a 1)
1.11 end;
2.1 --- a/src/HOL/Tools/Presburger/presburger.ML Sun Jun 06 18:35:39 2004 +0200
2.2 +++ b/src/HOL/Tools/Presburger/presburger.ML Sun Jun 06 18:36:36 2004 +0200
2.3 @@ -282,7 +282,7 @@
2.4 || Args.$$$ "abs" >> K (apsnd (K true));
2.5 in
2.6 Method.simple_args
2.7 - (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >>
2.8 + (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
2.9 curry (foldl op |>) (true, false))
2.10 (fn (q,a) => fn _ => meth q a 1)
2.11 end;