# HG changeset patch
# User wenzelm
# Date 1220802401 -7200
# Node ID cbc2cbfc840c07aa2626039b730c960b04af6ec5
# Parent  26bd1245a46b3c2981d5cd73ae87b0621f83feda
added no_interrupts;
tuned;

diff -r 26bd1245a46b -r cbc2cbfc840c src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Sep 07 17:46:40 2008 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Sep 07 17:46:41 2008 +0200
@@ -82,10 +82,11 @@
     [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce]
     (fn _ => f);
 
+val no_interrupts =
+  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
+
 fun uninterruptible f =
-  with_attributes
-    [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer]
-    (fn atts => f (fn g => with_attributes atts (fn _ => g)));
+  with_attributes no_interrupts (fn atts => f (fn g => with_attributes atts (fn _ => g)));
 
 
 (* execution with time limit *)
@@ -193,7 +194,7 @@
 fun self_critical () =
   (case ! critical_thread of
     NONE => false
-  | SOME id => Thread.equal (id, Thread.self ()));
+  | SOME t => Thread.equal (t, Thread.self ()));
 
 fun NAMED_CRITICAL name e =
   if self_critical () then e ()