src/HOL/Import/lazy_seq.ML
changeset 33339 d41f77196338
parent 32960 69916a850301
child 40627 becf5d5187cc
     1.1 --- a/src/HOL/Import/lazy_seq.ML	Thu Oct 29 23:49:55 2009 +0100
     1.2 +++ b/src/HOL/Import/lazy_seq.ML	Thu Oct 29 23:56:33 2009 +0100
     1.3 @@ -407,8 +407,8 @@
     1.4          make (fn () => copy (f x))
     1.5      end
     1.6  
     1.7 -fun EVERY fs = List.foldr (op THEN) succeed fs
     1.8 -fun FIRST fs = List.foldr (op 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 x =
    1.13      make (fn () =>