tuned;
authorwenzelm
Wed, 11 Oct 2023 14:03:16 +0200
changeset 78763 b7157c137855
parent 78762 89202852e52c
child 78764 a3dcae9a2ebe
tuned;
src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Wed Oct 11 13:49:08 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Wed Oct 11 14:03:16 2023 +0200
@@ -67,13 +67,15 @@
   val self_var = Thread_Data.var () : T Thread_Data.var;
 in
 
-fun init_self args =
-  let val t = make args in Thread_Data.put self_var (SOME t); t end;
+fun init_self name =
+  let
+    val t = make {thread = Thread.Thread.self (), name = name, id = make_id ()};
+  in Thread_Data.put self_var (SOME t); t end;
 
 fun self () =
   (case Thread_Data.get self_var of
     SOME t => t
-  | NONE => init_self {thread = Thread.Thread.self (), name = "", id = make_id ()});
+  | NONE => init_self "");
 
 fun is_self t = equal (t, self ());
 
@@ -116,8 +118,7 @@
     val self = Single_Assignment.var "self";
     fun main () =
       let
-        val name = params_name params;
-        val t = init_self {thread = Thread.Thread.self (), name = name, id = make_id ()};
+        val t = init_self (params_name params);
         val _ = Single_Assignment.assign self t;
       in body () end;
     val _ = Thread.Thread.fork (main, attributes params);