--- a/src/HOL/Integ/presburger.ML Sat May 29 15:08:21 2004 +0200
+++ b/src/HOL/Integ/presburger.ML Sat May 29 15:09:47 2004 +0200
@@ -282,7 +282,7 @@
|| Args.$$$ "abs" >> K (apsnd (K true));
in
Method.simple_args
- (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >>
+ (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
curry (foldl op |>) (true, false))
(fn (q,a) => fn _ => meth q a 1)
end;
--- a/src/HOL/Tools/Presburger/presburger.ML Sat May 29 15:08:21 2004 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML Sat May 29 15:09:47 2004 +0200
@@ -282,7 +282,7 @@
|| Args.$$$ "abs" >> K (apsnd (K true));
in
Method.simple_args
- (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >>
+ (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
curry (foldl op |>) (true, false))
(fn (q,a) => fn _ => meth q a 1)
end;