--- 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);