diff -r febd9234abdd -r 1bd90b76477a src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Mar 20 09:52:32 2009 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Mar 20 11:08:59 2009 +0100
@@ -77,11 +77,9 @@
 fun with_attributes new_atts f x =
   let
     val orig_atts = safe_interrupts (Thread.getAttributes ());
-    fun restore () = Thread.setAttributes orig_atts;
-    val result =
-      (Thread.setAttributes (safe_interrupts new_atts);
-        Exn.Result (f orig_atts x) before restore ())
-      handle e => Exn.Exn e before restore ();
+    val result = Exn.capture (fn () =>
+      (Thread.setAttributes (safe_interrupts new_atts); f orig_atts x)) ();
+    val _ = Thread.setAttributes orig_atts;
   in Exn.release result end;
 
 fun interruptible f = with_attributes regular_interrupts (fn _ => f);