# HG changeset patch
# User wenzelm
# Date 1683643148 -7200
# Node ID 1b1441e0354cf9d114cb9ba2cbae4bac213aa644
# Parent  1aa20895464ed64b82c4e00901c1d33579b8c689
more robust: publish token only after assignment of result;

diff -r 1aa20895464e -r 1b1441e0354c src/Pure/context.ML
--- a/src/Pure/context.ML	Tue May 09 16:33:30 2023 +0200
+++ b/src/Pure/context.ML	Tue May 09 16:39:08 2023 +0200
@@ -202,8 +202,9 @@
   if ! guard then
     let
       val token = Unsynchronized.ref (! token0);
-      val _ = Synchronized.change var (cons (Weak.weak (SOME token)));
-    in (token, fn res => (token := res; res)) end
+      fun assign res =
+        (token := res; Synchronized.change var (cons (Weak.weak (SOME token))); res);
+    in (token, assign) end
   else (token0, I);
 
 val theory_tokens = Synchronized.var "theory_tokens" ([]: theory Unsynchronized.weak_ref list);