src/Pure/goal.ML

   val protect: thm -> thm
   val conclude: thm -> thm
   val check_finished: Proof.context -> thm -> unit
   val finish: Proof.context -> thm -> thm
   val norm_result: thm -> thm
+  val fork_name: string -> (unit -> 'a) -> 'a future
   val fork: (unit -> 'a) -> 'a future
   val future_enabled: unit -> bool
   val local_future_enabled: unit -> bool
   val future_result: Proof.context -> thm future -> term -> thm
   val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm

   #> Drule.zero_var_indexes;
 
 
 (* parallel proofs *)
 
-fun fork e =
-  singleton (Future.forks {name = "Goal.fork", group = NONE, deps = [], pri = ~1})
+fun fork_name name e =
+  singleton (Future.forks {name = name, group = NONE, deps = [], pri = ~1})
     (fn () => Future.status e);
+
+fun fork e = fork_name "Goal.fork" e;
+
 
 val parallel_proofs = Unsynchronized.ref 1;
 
 fun future_enabled () =
   Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;