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,64 +1,68 @@
 (*  Title:      Pure/Concurrent/unsynchronized.ML
     Author:     Makarius
 
 Raw ML references as unsynchronized state variables.
 *)
 
 signature UNSYNCHRONIZED =
 sig
   datatype ref = datatype 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
   val weak_peek: 'a weak_ref -> 'a option
+  val weak_active: 'a weak_ref -> bool
 end;
 
 structure Unsynchronized: UNSYNCHRONIZED =
 struct
 
 (* regular references *)
 
 datatype ref = datatype 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) ();
 
 
 (* weak references *)
 
 (*see also $ML_SOURCES/basis/Weak.sml*)
 
 type 'a weak_ref = 'a ref option ref;
 
 fun weak_ref a = Weak.weak (SOME (ref a));
 
 fun weak_peek (ref (SOME (ref a))) = SOME a
   | weak_peek _ = NONE;
 
+fun weak_active (ref (SOME (ref _))) = true
+  | weak_active _ = false;
+
 end;
 
 ML_Name_Space.forget_val "ref";
 ML_Name_Space.forget_type "ref";