src/Pure/General/seq.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 16002 e0557c452138
     1.1 --- a/src/Pure/General/seq.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/Pure/General/seq.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -97,7 +97,7 @@
     1.4    | SOME (x, xq') => x :: list_of xq');
     1.5  
     1.6  (*conversion from list to sequence*)
     1.7 -fun of_list xs = Library.foldr cons (xs, empty);
     1.8 +fun of_list xs = foldr cons empty xs;
     1.9  
    1.10  
    1.11  (*map the function f over the sequence, making a new sequence*)
    1.12 @@ -203,8 +203,8 @@
    1.13  fun op APPEND (f, g) x =
    1.14    append (f x, make (fn () => pull (g x)));
    1.15  
    1.16 -fun EVERY fs = Library.foldr THEN (fs, succeed);
    1.17 -fun FIRST fs = Library.foldr ORELSE (fs, fail);
    1.18 +fun EVERY fs = foldr THEN succeed fs;
    1.19 +fun FIRST fs = foldr ORELSE fail fs;
    1.20  
    1.21  fun TRY f = ORELSE (f, succeed);
    1.22