# HG changeset patch
# User wenzelm
# Date 1086539796 -7200
# Node ID e0e2361b9a30b225b516d0a50b7098d7eca7528d
# Parent  e1f501a141593e170d2d42a3cc4783153d38b5c6
avoid Args.list (lost update?);

diff -r e1f501a14159 -r e0e2361b9a30 src/HOL/Integ/presburger.ML
--- 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;
diff -r e1f501a14159 -r e0e2361b9a30 src/HOL/Tools/Presburger/presburger.ML
--- 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;