src/Pure/ML-Systems/multithreading_polyml.ML
changeset 25735 4d147263f71f
parent 25704 df9c8074ff09
child 25775 90525e67ede7
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Dec 20 21:12:01 2007 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Dec 20 21:12:02 2007 +0100
     1.3 @@ -257,6 +257,12 @@
     1.4  
     1.5  end;
     1.6  
     1.7 +
     1.8 +(* thread data *)
     1.9 +
    1.10 +val get_data = Thread.getLocal;
    1.11 +val put_data = Thread.setLocal;
    1.12 +
    1.13  end;
    1.14  
    1.15  structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;