src/Pure/goal.ML

   val protect: thm -> thm
   val conclude: thm -> thm
   val check_finished: Proof.context -> thm -> thm
   val finish: Proof.context -> thm -> thm
   val norm_result: thm -> thm
-  val fork_name: string -> int -> (unit -> 'a) -> 'a future
+  val fork_params: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
   val fork: int -> (unit -> 'a) -> 'a future
   val peek_futures: serial -> unit future list
   val reset_futures: unit -> Future.group list
   val shutdown_futures: unit -> unit
   val future_enabled_level: int -> bool

   let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
   in Output.status (implode (map (Markup.markup_only o props) markups)) end;
 
 in
 
-fun fork_name name pri e =
+fun fork_params {name, pos, pri} e =
   uninterruptible (fn _ => fn () =>
     let
-      val pos = Position.thread_data ();
       val id = the_default 0 (Position.parse_id pos);
       val _ = count_forked 1;
 
       val future =
         (singleton o Future.forks)

             in Exn.release result end);
       val _ = status (Future.task_of future) [Markup.forked];
       val _ = register_forked id future;
     in future end) ();
 
-fun fork pri e = fork_name "Goal.fork" pri e;
+fun fork pri e =
+  fork_params {name = "Goal.fork", pos = Position.thread_data (), pri = pri} e;
 
 fun forked_count () = #1 (Synchronized.value forked_proofs);
 
 fun peek_futures id =
   Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;