# HG changeset patch
# User wenzelm
# Date 1296514387 -3600
# Node ID fa0da47131d213b4049d94387bdd3b0e61f639a1
# Parent  4639f40b20c9b5f073fb3aaa1b440d221d40a573
more specific Goal.fork_name;

diff -r 4639f40b20c9 -r fa0da47131d2 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Jan 31 23:21:43 2011 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Jan 31 23:53:07 2011 +0100
@@ -1100,7 +1100,8 @@
 fun future_terminal_proof proof1 proof2 meths int state =
   if int orelse is_relevant state orelse not (Goal.local_future_enabled ())
   then proof1 meths state
-  else snd (proof2 (fn state' => Goal.fork (fn () => ((), proof1 meths state'))) state);
+  else snd (proof2 (fn state' =>
+    Goal.fork_name "Proof.future_terminal_proof" (fn () => ((), proof1 meths state'))) state);
 
 in
 
diff -r 4639f40b20c9 -r fa0da47131d2 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon Jan 31 23:21:43 2011 +0100
+++ b/src/Pure/goal.ML	Mon Jan 31 23:53:07 2011 +0100
@@ -23,6 +23,7 @@
   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
@@ -106,10 +107,13 @@
 
 (* 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 () =