diff -r 1a5e364584ae -r 5db89f8d44f3 src/Pure/Concurrent/synchronized_sequential.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/synchronized_sequential.ML	Thu Oct 01 18:21:11 2009 +0200
@@ -0,0 +1,27 @@
+(*  Title:      Pure/Concurrent/synchronized_sequential.ML
+    Author:     Makarius
+
+Sequential version of state variables -- plain refs.
+*)
+
+structure Synchronized: SYNCHRONIZED =
+struct
+
+abstype 'a var = Var of 'a Unsynchronized.ref
+with
+
+fun var _ x = Var (Unsynchronized.ref x);
+fun value (Var var) = ! var;
+
+fun timed_access (Var var) _ f =
+  (case f (! var) of
+    SOME (y, x') => (var := x'; SOME y)
+  | NONE => Thread.unavailable ());
+
+fun guarded_access var f = the (timed_access var (K NONE) f);
+
+fun change_result var f = guarded_access var (SOME o f);
+fun change var f = change_result var (fn x => ((), f x));
+
+end;
+end;