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