| 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