src/Pure/Concurrent/unsynchronized.ML

--- a/src/Pure/Concurrent/unsynchronized.ML	Mon May 08 21:11:01 2023 +0200
+++ b/src/Pure/Concurrent/unsynchronized.ML	Mon May 08 21:50:21 2023 +0200
@@ -7,6 +7,7 @@
 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
@@ -22,6 +23,8 @@
 
 datatype ref = datatype ref;
 
+type 'a weak_ref = 'a ref option ref;
+
 val op := = op :=;
 val ! = !;