avoid Args.list (lost update?);
authorwenzelm
Sun, 06 Jun 2004 18:36:36 +0200
changeset 14882e0e2361b9a30
parent 14881 e1f501a14159
child 14883 ca000a495448
avoid Args.list (lost update?);
src/HOL/Integ/presburger.ML
src/HOL/Tools/Presburger/presburger.ML
     1.1 --- a/src/HOL/Integ/presburger.ML	Sun Jun 06 18:35:39 2004 +0200
     1.2 +++ b/src/HOL/Integ/presburger.ML	Sun Jun 06 18:36:36 2004 +0200
     1.3 @@ -282,7 +282,7 @@
     1.4        || Args.$$$ "abs" >> K (apsnd (K true));
     1.5   in
     1.6     Method.simple_args 
     1.7 -  (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >>
     1.8 +  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
     1.9      curry (foldl op |>) (true, false))
    1.10      (fn (q,a) => fn _ => meth q a 1)
    1.11    end;
     2.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Sun Jun 06 18:35:39 2004 +0200
     2.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Sun Jun 06 18:36:36 2004 +0200
     2.3 @@ -282,7 +282,7 @@
     2.4        || Args.$$$ "abs" >> K (apsnd (K true));
     2.5   in
     2.6     Method.simple_args 
     2.7 -  (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >>
     2.8 +  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
     2.9      curry (foldl op |>) (true, false))
    2.10      (fn (q,a) => fn _ => meth q a 1)
    2.11    end;