diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/General/seq.ML --- a/src/Pure/General/seq.ML Fri Mar 04 11:44:26 2005 +0100 +++ b/src/Pure/General/seq.ML Fri Mar 04 15:07:34 2005 +0100 @@ -97,7 +97,7 @@ | SOME (x, xq') => x :: list_of xq'); (*conversion from list to sequence*) -fun of_list xs = Library.foldr cons (xs, empty); +fun of_list xs = foldr cons empty xs; (*map the function f over the sequence, making a new sequence*) @@ -203,8 +203,8 @@ fun op APPEND (f, g) x = append (f x, make (fn () => pull (g x))); -fun EVERY fs = Library.foldr THEN (fs, succeed); -fun FIRST fs = Library.foldr ORELSE (fs, fail); +fun EVERY fs = foldr THEN succeed fs; +fun FIRST fs = foldr ORELSE fail fs; fun TRY f = ORELSE (f, succeed);