--- 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
--- 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 () =