# HG changeset patch
# User wenzelm
# Date 1695308988 -7200
# Node ID 5b2391321bab512e4e991a99826385880ac7f691
# Parent  1b9e0f74addbe2c5edea4ec27ce5399e15a7275c
tuned;

diff -r 1b9e0f74addb -r 5b2391321bab src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Thu Sep 21 17:04:56 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Thu Sep 21 17:09:48 2023 +0200
@@ -53,14 +53,13 @@
   val self_var = Thread_Data.var () : T Thread_Data.var;
 in
 
-fun set_self t = Thread_Data.put self_var (SOME t);
+fun init_self args =
+  let val t = make args in Thread_Data.put self_var (SOME t); t end;
 
 fun self () =
   (case Thread_Data.get self_var of
     SOME t => t
-  | NONE =>
-      let val t = make {thread = Thread.Thread.self (), name = "", id = make_id ()}
-      in set_self t; t end);
+  | NONE => init_self {thread = Thread.Thread.self (), name = "", id = make_id ()});
 
 fun is_self t = equal (t, self ());
 
@@ -87,8 +86,7 @@
     val self = Single_Assignment.var "self";
     fun main () =
       let
-        val t = make {thread = Thread.Thread.self (), name = #name params, id = make_id ()};
-        val _ = set_self t;
+        val t = init_self {thread = Thread.Thread.self (), name = #name params, id = make_id ()};
         val _ = Single_Assignment.assign self t;
       in body () end;
     val _ = Thread.Thread.fork (main, attributes params);