--- a/src/HOL/Integ/presburger.ML Sun Jun 06 18:35:39 2004 +0200
+++ b/src/HOL/Integ/presburger.ML Sun Jun 06 18:36:36 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 Sun Jun 06 18:35:39 2004 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML Sun Jun 06 18:36:36 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;