src/Pure/General/lazy.ML
changeset 32738 15bb09ca0378
parent 29422 fdf396a24a9f
     1.1 --- a/src/Pure/General/lazy.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/General/lazy.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -26,12 +26,12 @@
     1.4    Lazy of unit -> 'a |
     1.5    Result of 'a Exn.result;
     1.6  
     1.7 -type 'a lazy = 'a T ref;
     1.8 +type 'a lazy = 'a T Unsynchronized.ref;
     1.9  
    1.10  fun same (r1: 'a lazy, r2) = r1 = r2;
    1.11  
    1.12 -fun lazy e = ref (Lazy e);
    1.13 -fun value x = ref (Result (Exn.Result x));
    1.14 +fun lazy e = Unsynchronized.ref (Lazy e);
    1.15 +fun value x = Unsynchronized.ref (Result (Exn.Result x));
    1.16  
    1.17  fun peek r =
    1.18    (case ! r of