diff --git a/src/Pure/Concurrent/synchronized.ML b/src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML
+++ b/src/Pure/Concurrent/synchronized.ML
@@ -1,95 +1,118 @@
 (*  Title:      Pure/Concurrent/synchronized.ML
     Author:     Fabian Immler and Makarius
 
 Synchronized variables.
 *)
 
 signature SYNCHRONIZED =
 sig
   type 'a var
   val var: string -> 'a -> 'a var
   val value: 'a var -> 'a
   val assign: 'a var -> 'a -> unit
   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 change_result: 'a var -> ('a -> 'b * 'a) -> 'b
   val change: 'a var -> ('a -> 'a) -> unit
+  type 'a cache
+  val cache: (unit -> 'a) -> 'a cache
+  val cache_eval: 'a cache -> 'a
 end;
 
 structure Synchronized: SYNCHRONIZED =
 struct
 
 (* state variable *)
 
 datatype 'a state =
     Immutable of 'a
   | Mutable of {lock: Mutex.mutex, cond: ConditionVar.conditionVar, content: 'a};
 
 fun init_state x =
   Mutable {lock = Mutex.mutex (), cond = ConditionVar.conditionVar (), content = x};
 
 fun immutable_fail name = raise Fail ("Illegal access to immutable value " ^ name);
 
 abstype 'a var = Var of {name: string, state: 'a state Unsynchronized.ref}
 with
 
 fun var name x =
   Var {name = name, state = Unsynchronized.ref (init_state x)};
 
 fun value (Var {name, state}) =
   (case ! state of
     Immutable x => x
   | Mutable {lock, ...} =>
       Multithreading.synchronized name lock (fn () =>
         (case ! state of
           Immutable x => x
         | Mutable {content, ...} => content)));
 
 fun assign (Var {name, state}) x =
   (case ! state of
     Immutable _ => immutable_fail name
   | Mutable {lock, cond, ...} =>
       Multithreading.synchronized name lock (fn () =>
         (case ! state of
           Immutable _ => immutable_fail name
         | Mutable _ =>
             Thread_Attributes.uninterruptible (fn _ => fn () =>
              (state := Immutable x; RunCall.clearMutableBit state;
                ConditionVar.broadcast cond)) ())));
 
 
 (* synchronized access *)
 
 fun timed_access (Var {name, state}) time_limit f =
   (case ! state of
     Immutable _ => immutable_fail name
   | Mutable {lock, cond, ...} =>
       Multithreading.synchronized name lock (fn () =>
         let
           fun try_change () =
             (case ! state of
               Immutable _ => immutable_fail name
             | Mutable {content = x, ...} =>
                 (case f x of
                   NONE =>
                     (case Multithreading.sync_wait (time_limit x) cond lock of
                       Exn.Res true => try_change ()
                     | Exn.Res false => NONE
                     | Exn.Exn exn => Exn.reraise exn)
                 | SOME (y, x') =>
                     Thread_Attributes.uninterruptible (fn _ => fn () =>
                       (state := Mutable {lock = lock, cond = cond, content = x'};
                         ConditionVar.broadcast cond; SOME y)) ()));
         in try_change () end));
 
 fun guarded_access var f = the (timed_access var (fn _ => NONE) f);
 
 
 (* unconditional change *)
 
 fun change_result var f = guarded_access var (SOME o f);
 fun change var f = change_result var (fn x => ((), f x));
 
 end;
 
+
+(* cached evaluation via weak_ref *)
+
+abstype 'a cache =
+  Cache of {expr: unit -> 'a, var: 'a Unsynchronized.weak_ref option var}
+with
+
+fun cache expr =
+  Cache {expr = expr, var = var "Synchronized.cache" NONE};
+
+fun cache_eval (Cache {expr, var}) =
+  change_result var (fn state =>
+    (case state of
+      SOME (Unsynchronized.ref (SOME (Unsynchronized.ref result))) => (result, state)
+    | _ =>
+      let val result = expr ()
+      in (result, SOME (Unsynchronized.weak_ref result)) end));
+
 end;
+
+end;
diff --git a/src/Pure/Concurrent/unsynchronized.ML b/src/Pure/Concurrent/unsynchronized.ML
--- a/src/Pure/Concurrent/unsynchronized.ML
+++ b/src/Pure/Concurrent/unsynchronized.ML
@@ -1,50 +1,52 @@
 (*  Title:      Pure/Concurrent/unsynchronized.ML
     Author:     Makarius
 
 Raw ML references as unsynchronized state variables.
 *)
 
 signature UNSYNCHRONIZED =
 sig
   datatype ref = datatype ref
-  type 'a weak_ref = 'a ref option ref
   val := : 'a ref * 'a -> unit
   val ! : 'a ref -> 'a
   val change: 'a ref -> ('a -> 'a) -> unit
   val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b
   val inc: int ref -> int
   val dec: int ref -> int
   val add: int ref -> int -> int
   val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
+  type 'a weak_ref = 'a ref option ref
+  val weak_ref: 'a -> 'a weak_ref
 end;
 
 structure Unsynchronized: UNSYNCHRONIZED =
 struct
 
 datatype ref = datatype ref;
 
-type 'a weak_ref = 'a ref option ref;
-
 val op := = op :=;
 val ! = !;
 
 fun change r f = r := f (! r);
 fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
 
 fun inc i = (i := ! i + (1: int); ! i);
 fun dec i = (i := ! i - (1: int); ! i);
 fun add i n = (i := ! i + (n: int); ! i);
 
 fun setmp flag value f x =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val orig_value = ! flag;
       val _ = flag := value;
       val result = Exn.capture (restore_attributes f) x;
       val _ = flag := orig_value;
     in Exn.release result end) ();
 
+type 'a weak_ref = 'a ref option ref;
+fun weak_ref a = Weak.weak (SOME (ref a));
+
 end;
 
 ML_Name_Space.forget_val "ref";
 ML_Name_Space.forget_type "ref";