src/Pure/Concurrent/standard_thread.ML
changeset 62889 99c7f31615c2
parent 62505 9e2a65912111
child 62923 3a122e1e352a
     1.1 --- a/src/Pure/Concurrent/standard_thread.ML	Wed Apr 06 14:08:57 2016 +0200
     1.2 +++ b/src/Pure/Concurrent/standard_thread.ML	Wed Apr 06 16:33:33 2016 +0200
     1.3 @@ -27,11 +27,11 @@
     1.4  (* unique name *)
     1.5  
     1.6  local
     1.7 -  val tag = Universal.tag () : string Universal.tag;
     1.8 +  val name_var = Thread_Data.var () : string Thread_Data.var;
     1.9    val count = Counter.make ();
    1.10  in
    1.11  
    1.12 -fun get_name () = Thread.getLocal tag;
    1.13 +fun get_name () = Thread_Data.get name_var;
    1.14  
    1.15  fun the_name () =
    1.16    (case get_name () of
    1.17 @@ -39,7 +39,7 @@
    1.18    | SOME name => name);
    1.19  
    1.20  fun set_name base =
    1.21 -  Thread.setLocal (tag, base ^ "/" ^ string_of_int (count ()));
    1.22 +  Thread_Data.put name_var (SOME (base ^ "/" ^ string_of_int (count ())));
    1.23  
    1.24  end;
    1.25