src/Pure/ML-Systems/multithreading_polyml.ML

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Dec 20 21:12:01 2007 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Dec 20 21:12:02 2007 +0100
@@ -257,6 +257,12 @@
 
 end;
 
+
+(* thread data *)
+
+val get_data = Thread.getLocal;
+val put_data = Thread.setLocal;
+
 end;
 
 structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;