Pure/sequence: added comment explaining that memoing sequences were found
to be much slower (due to overheads) than the sequences currently used.
--- a/src/Pure/sequence.ML Mon Nov 21 11:27:10 1994 +0100
+++ b/src/Pure/sequence.ML Mon Nov 21 11:33:23 1994 +0100
@@ -2,12 +2,12 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1988 University of Cambridge
-*)
+
+Unbounded sequences implemented by closures.
-(*Unbounded sequences implemented by closures.
+RECOMPUTES if sequence is re-inspected.
- Could use 'a seq = Seq of ('a * (unit -> 'a seq)) option.
- Recomputes if sequence is re-inspected; memoing would need polymorphic refs.
+Memoing, using polymorphic refs, was found to be slower! (More GCs)
*)