# HG changeset patch
# User wenzelm
# Date 1190407873 -7200
# Node ID f311717d1f03470efe8956f246e6a80d362c4817
# Parent  35075a1e9599205c6c22a6e5b270af403406a60a
tuned;

diff -r 35075a1e9599 -r f311717d1f03 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Sep 21 22:51:12 2007 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Sep 21 22:51:13 2007 +0200
@@ -133,16 +133,11 @@
 datatype 'a task =
   Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
 
-local
-
-val protected_name = ref "";
-
-in
-
 fun schedule n next_task = uninterruptible (fn _ => fn tasks =>
   let
     (*protected execution*)
     val lock = Mutex.mutex ();
+    val protected_name = ref "";
     fun PROTECTED name e =
       let
         val name' = ! protected_name;
@@ -219,8 +214,6 @@
 
 end;
 
-end;
-
 val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
 val CRITICAL = Multithreading.CRITICAL;
 val ignore_interrupt = Multithreading.ignore_interrupt;