avoid Args.list (lost update?);
authorwenzelm
Sun, 06 Jun 2004 18:36:36 +0200
changeset 14882 e0e2361b9a30
parent 14881 e1f501a14159
child 14883 ca000a495448
avoid Args.list (lost update?);
src/HOL/Integ/presburger.ML
src/HOL/Tools/Presburger/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;
--- 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;