avoid Args.list;
authorwenzelm
Sat, 29 May 2004 15:09:47 +0200
changeset 14841 37fc364a60c3
parent 14840 dc23ff2629e2
child 14842 3a1fe2c524d0
avoid Args.list;
src/HOL/Integ/presburger.ML
src/HOL/Tools/Presburger/presburger.ML
--- 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;