diff -r 5df3607867c1 -r b293e3ed3cad src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Jan 02 23:00:57 2008 +0100
+++ b/src/Pure/library.ML	Thu Jan 03 00:15:39 2008 +0100
@@ -65,6 +65,7 @@
   val change: 'a ref -> ('a -> 'a) -> unit
   val setmp_noncritical: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
   val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
+  val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
 
   (*lists*)
   exception UnequalLengths
@@ -338,6 +339,13 @@
 
 fun setmp flag value f x = NAMED_CRITICAL "setmp" (fn () => setmp_noncritical flag value f x);
 
+fun setmp_thread_data tag orig_data data f x =
+  let
+    val _ = Multithreading.put_data (tag, data);
+    val result = Exn.capture f x;
+    val _ = Multithreading.put_data (tag, orig_data);
+  in Exn.release result end;
+
 
 
 (** lists **)