1.1 --- a/src/Pure/Concurrent/future.ML	Mon Nov 11 16:40:07 2013 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Wed Nov 20 22:10:45 2013 +0100
     1.3 @@ -48,8 +48,7 @@
     1.4    val worker_group: unit -> group option
     1.5    val the_worker_group: unit -> group
     1.6    val worker_subgroup: unit -> group
     1.7 -  val worker_nest: string -> ('a -> 'b) -> 'a -> 'b
     1.8 -  val worker_guest: string -> group -> ('a -> 'b) -> 'a -> 'b
     1.9 +  val worker_context: string -> group -> ('a -> 'b) -> 'a -> 'b
    1.10    type 'a future
    1.11    val task_of: 'a future -> task
    1.12    val peek: 'a future -> 'a Exn.result option
    1.13 @@ -110,13 +109,8 @@
    1.14  
    1.15  fun worker_subgroup () = new_group (worker_group ());
    1.16  
    1.17 -fun worker_nest name f x =
    1.18 -  setmp_worker_task (Task_Queue.new_task (the_worker_group ()) name NONE) f x;
    1.19 -
    1.20 -fun worker_guest name group f x =
    1.21 -  if is_some (worker_task ()) then
    1.22 -    raise Fail "Already running as worker thread"
    1.23 -  else setmp_worker_task (Task_Queue.new_task group name NONE) f x;
    1.24 +fun worker_context name group f x =
    1.25 +  setmp_worker_task (Task_Queue.new_task group name NONE) f x;
    1.26  
    1.27  fun worker_joining e =
    1.28    (case worker_task () of