more robust: prefer linear data flow;

--- a/src/Pure/Concurrent/isabelle_thread.ML	Wed Sep 20 17:40:09 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Thu Sep 21 17:04:56 2023 +0200
@@ -84,11 +84,15 @@
 
 fun fork (params: params) body =
   let
-    val name = #name params;
-    val id = make_id ();
-    fun main () = (set_self (make {thread = Thread.Thread.self (), name = name, id = id}); body ());
-    val thread = Thread.Thread.fork (main, attributes params);
-  in make {thread = thread, name = name, id = id} end;
+    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 _ = Single_Assignment.assign self t;
+      in body () end;
+    val _ = Thread.Thread.fork (main, attributes params);
+  in Single_Assignment.await self end;
 
 
 (* join *)

--- a/src/Pure/ROOT.ML	Wed Sep 20 17:40:09 2023 +0200
+++ b/src/Pure/ROOT.ML	Thu Sep 21 17:04:56 2023 +0200
@@ -121,8 +121,8 @@
 ML_file_no_debug "ML/exn_debugger.ML";
 
 ML_file "Concurrent/thread_data_virtual.ML";
+ML_file "Concurrent/single_assignment.ML";
 ML_file "Concurrent/isabelle_thread.ML";
-ML_file "Concurrent/single_assignment.ML";
 
 ML_file "Concurrent/par_exn.ML";
 ML_file "Concurrent/task_queue.ML";