src/Pure/Concurrent/synchronized_dummy.ML
changeset 32738 15bb09ca0378
parent 32736 f126e68d003d
     1.1 --- a/src/Pure/Concurrent/synchronized_dummy.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/synchronized_dummy.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -7,9 +7,9 @@
     1.4  structure Synchronized: SYNCHRONIZED =
     1.5  struct
     1.6  
     1.7 -datatype 'a var = Var of 'a ref;
     1.8 +datatype 'a var = Var of 'a Unsynchronized.ref;
     1.9  
    1.10 -fun var _ x = Var (ref x);
    1.11 +fun var _ x = Var (Unsynchronized.ref x);
    1.12  fun value (Var var) = ! var;
    1.13  
    1.14  fun timed_access (Var var) _ f =