src/Pure/General/seq.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/Pure/General/seq.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/General/seq.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -71,8 +71,8 @@
     1.4  fun single x = cons (x, empty);
     1.5  
     1.6  (*head and tail -- beware of calling the sequence function twice!!*)
     1.7 -fun hd xq = #1 (the (pull xq))
     1.8 -and tl xq = #2 (the (pull xq));
     1.9 +fun hd xq = #1 (valOf (pull xq))
    1.10 +and tl xq = #2 (valOf (pull xq));
    1.11  
    1.12  (*partial function as procedure*)
    1.13  fun try f x =
    1.14 @@ -97,7 +97,7 @@
    1.15    | SOME (x, xq') => x :: list_of xq');
    1.16  
    1.17  (*conversion from list to sequence*)
    1.18 -fun of_list xs = foldr cons (xs, empty);
    1.19 +fun of_list xs = Library.foldr cons (xs, empty);
    1.20  
    1.21  
    1.22  (*map the function f over the sequence, making a new sequence*)
    1.23 @@ -203,8 +203,8 @@
    1.24  fun op APPEND (f, g) x =
    1.25    append (f x, make (fn () => pull (g x)));
    1.26  
    1.27 -fun EVERY fs = foldr THEN (fs, succeed);
    1.28 -fun FIRST fs = foldr ORELSE (fs, fail);
    1.29 +fun EVERY fs = Library.foldr THEN (fs, succeed);
    1.30 +fun FIRST fs = Library.foldr ORELSE (fs, fail);
    1.31  
    1.32  fun TRY f = ORELSE (f, succeed);
    1.33