removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
access: uninterruptible update/broadcast, to prevent lost signals;

--- a/src/Pure/Concurrent/synchronized.ML	Sat Feb 06 22:01:48 2010 +0100
+++ b/src/Pure/Concurrent/synchronized.ML	Sat Feb 06 22:05:02 2010 +0100
@@ -11,10 +11,8 @@
   val value: 'a var -> 'a
   val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
   val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
-  val readonly_access: 'a var -> ('a -> 'b option) -> 'b
   val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
   val change: 'a var -> ('a -> 'a) -> unit
-  val assign: 'a var -> ('a -> 'a) -> unit
 end;
 
 structure Synchronized: SYNCHRONIZED =
@@ -22,11 +20,12 @@
 
 (* state variables *)
 
-datatype 'a var = Var of
+abstype 'a var = Var of
  {name: string,
   lock: Mutex.mutex,
   cond: ConditionVar.conditionVar,
-  var: 'a Unsynchronized.ref};
+  var: 'a Unsynchronized.ref}
+with
 
 fun var name x = Var
  {name = name,
@@ -39,7 +38,7 @@
 
 (* synchronized access *)
 
-fun access {time_limit, readonly, finish} (Var {name, lock, cond, var}) f =
+fun timed_access (Var {name, lock, cond, var}) time_limit f =
   SimpleThread.synchronized name lock (fn () =>
     let
       fun try_change () =
@@ -51,36 +50,19 @@
               | Exn.Result false => NONE
               | Exn.Exn exn => reraise exn)
           | SOME (y, x') =>
-              if readonly then SOME y
-              else
-                let
-                  val _ = magic_immutability_test var
-                    andalso raise Fail ("Attempt to change finished variable " ^ quote name);
-                  val _ = var := x';
-                  val _ = if finish then magic_immutability_mark var else ();
-                in SOME y end)
+              uninterruptible (fn _ => fn () =>
+                (var := x'; ConditionVar.broadcast cond; SOME y)) ())
         end;
-      val res = try_change ();
-      val _ = ConditionVar.broadcast cond;
-    in res end);
-
-fun timed_access var time_limit f =
-  access {time_limit = time_limit, readonly = false, finish = false} var f;
+    in try_change () end);
 
 fun guarded_access var f = the (timed_access var (K NONE) f);
 
-fun readonly_access var f =
-  the (access {time_limit = K NONE, readonly = true, finish = false} var
-    (fn x => (case f x of NONE => NONE | SOME y => SOME (y, x))));
-
 
 (* unconditional change *)
 
 fun change_result var f = guarded_access var (SOME o f);
 fun change var f = change_result var (fn x => ((), f x));
 
-fun assign var f =
-  the (access {time_limit = K NONE, readonly = false, finish = true} var
-    (fn x => SOME ((), f x)));
+end;
 
 end;

--- a/src/Pure/Concurrent/synchronized_sequential.ML	Sat Feb 06 22:01:48 2010 +0100
+++ b/src/Pure/Concurrent/synchronized_sequential.ML	Sat Feb 06 22:05:02 2010 +0100
@@ -20,13 +20,8 @@
 
 fun guarded_access var f = the (timed_access var (K NONE) f);
 
-fun readonly_access var f =
-  guarded_access var (fn x => (case f x of NONE => NONE | SOME y => SOME (y, x)));
-
 fun change_result var f = guarded_access var (SOME o f);
 fun change var f = change_result var (fn x => ((), f x));
 
-val assign = change;
-
 end;
 end;