src/Pure/goal.ML

--- a/src/Pure/goal.ML	Wed Apr 03 20:56:08 2013 +0200
+++ b/src/Pure/goal.ML	Wed Apr 03 21:30:32 2013 +0200
@@ -26,7 +26,7 @@
   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
@@ -143,10 +143,9 @@
 
 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;
 
@@ -176,7 +175,8 @@
       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);