src/Pure/General/seq.ML
changeset 19475 8aa2b380614a
parent 17347 fb3d42ef61ed
child 19484 89484a62184a
     1.1 --- a/src/Pure/General/seq.ML	Wed Apr 26 22:38:11 2006 +0200
     1.2 +++ b/src/Pure/General/seq.ML	Wed Apr 26 22:38:16 2006 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4    val make: (unit -> ('a * 'a seq) option) -> 'a seq
     1.5    val pull: 'a seq -> ('a * 'a seq) option
     1.6    val empty: 'a seq
     1.7 -  val cons: 'a * 'a seq -> 'a seq
     1.8 +  val cons: 'a -> 'a seq -> 'a seq
     1.9    val single: 'a -> 'a seq
    1.10    val try: ('a -> 'b) -> 'a -> 'b seq
    1.11    val hd: 'a seq -> 'a
    1.12 @@ -70,9 +70,9 @@
    1.13  (*prefix an element to the sequence -- use cons (x, xq) only if
    1.14    evaluation of xq need not be delayed, otherwise use
    1.15    make (fn () => SOME (x, xq))*)
    1.16 -fun cons x_xq = make (fn () => SOME x_xq);
    1.17 +fun cons x xq = make (fn () => SOME (x, xq));
    1.18  
    1.19 -fun single x = cons (x, empty);
    1.20 +fun single x = cons x empty;
    1.21  
    1.22  (*head and tail -- beware of calling the sequence function twice!!*)
    1.23  fun hd xq = #1 (the (pull xq))
    1.24 @@ -101,7 +101,7 @@
    1.25    | SOME (x, xq') => x :: list_of xq');
    1.26  
    1.27  (*conversion from list to sequence*)
    1.28 -fun of_list xs = foldr cons empty xs;
    1.29 +fun of_list xs = fold_rev cons xs empty;
    1.30  
    1.31  
    1.32  (*sequence append:  put the elements of xq in front of those of yq*)
    1.33 @@ -239,6 +239,6 @@
    1.34  fun DETERM f x =
    1.35    (case pull (f x) of
    1.36      NONE => empty
    1.37 -  | SOME (x', _) => cons (x', empty));
    1.38 +  | SOME (x', _) => cons x' empty);
    1.39  
    1.40  end;