| changeset 28971 | 300ec36a19af |
| parent 28673 | d746a8c12c43 |
| child 30190 | 479806475f3c |
--- a/src/HOL/Import/lazy_seq.ML Tue Dec 02 14:29:12 2008 +0100 +++ b/src/HOL/Import/lazy_seq.ML Thu Dec 04 23:00:21 2008 +0100 @@ -80,7 +80,7 @@ structure LazySeq :> LAZY_SEQ = struct -datatype 'a seq = Seq of ('a * 'a seq) option Lazy.T +datatype 'a seq = Seq of ('a * 'a seq) option lazy exception Empty