src/Pure/ML-Systems/multithreading_polyml.ML
changeset 24672 f311717d1f03
parent 24668 4058b7b0925c
child 24688 a5754ca5c510
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Sep 21 22:51:12 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Sep 21 22:51:13 2007 +0200
     1.3 @@ -133,16 +133,11 @@
     1.4  datatype 'a task =
     1.5    Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
     1.6  
     1.7 -local
     1.8 -
     1.9 -val protected_name = ref "";
    1.10 -
    1.11 -in
    1.12 -
    1.13  fun schedule n next_task = uninterruptible (fn _ => fn tasks =>
    1.14    let
    1.15      (*protected execution*)
    1.16      val lock = Mutex.mutex ();
    1.17 +    val protected_name = ref "";
    1.18      fun PROTECTED name e =
    1.19        let
    1.20          val name' = ! protected_name;
    1.21 @@ -219,8 +214,6 @@
    1.22  
    1.23  end;
    1.24  
    1.25 -end;
    1.26 -
    1.27  val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
    1.28  val CRITICAL = Multithreading.CRITICAL;
    1.29  val ignore_interrupt = Multithreading.ignore_interrupt;