author | wenzelm |
Sat, 22 Nov 1997 13:26:43 +0100 | |
changeset 4279 | 835ea07170a6 |
parent 4278 | c64867c093fb |
child 4280 | 278660f52716 |
src/Pure/seq.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/seq.ML Sat Nov 22 13:26:30 1997 +0100 +++ b/src/Pure/seq.ML Sat Nov 22 13:26:43 1997 +0100 @@ -44,7 +44,7 @@ (*the empty sequence*) -val empty = make (fn () => None); +val empty = Seq (fn () => None); (*prefix an element to the sequence -- use cons (x, xq) only if evaluation of xq need not be delayed, otherwise use