src/Pure/General/seq.ML
changeset 23178 07ba6b58b3d2
parent 21395 f34ac19659ae
child 25955 94a515ed8a39
     1.1 --- a/src/Pure/General/seq.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Pure/General/seq.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -202,8 +202,8 @@
     1.4  fun op APPEND (f, g) x =
     1.5    append (f x) (make (fn () => pull (g x)));
     1.6  
     1.7 -fun EVERY fs = foldr THEN succeed fs;
     1.8 -fun FIRST fs = foldr ORELSE fail fs;
     1.9 +fun EVERY fs = fold_rev (curry op THEN) fs succeed;
    1.10 +fun FIRST fs = fold_rev (curry op ORELSE) fs fail;
    1.11  
    1.12  fun TRY f = ORELSE (f, succeed);
    1.13