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: (unit -> 'a) -> 'a future
   val future_enabled: unit -> bool
   val local_future_enabled: unit -> bool
+  val local_future_enforced: unit -> bool
   val future_result: Proof.context -> thm future -> term -> thm
   val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
   val prove_multi: Proof.context -> string list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm list
   val prove_future: Proof.context -> string list -> term list -> term ->

   #> MetaSimplifier.norm_hhf_protect
   #> Thm.strip_shyps
   #> Drule.zero_var_indexes;
 
 
-(* future_enabled *)
+(* parallel proofs *)
+
+fun fork e = Future.fork_pri ~1 (fn () =>
+  let
+    val _ = Output.status (Markup.markup Markup.forked "");
+    val x = e ();  (*sic*)
+    val _ = Output.status (Markup.markup Markup.joined "");
+  in x end);
 
 val parallel_proofs = Unsynchronized.ref 1;
 
 fun future_enabled () =
   Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
 
 fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;
+fun local_future_enforced () = future_enabled () andalso ! parallel_proofs >= 3;
 
 
 (* future_result *)
 
 fun future_result ctxt result prop =

             else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
           end);
     val res =
       if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
       then result ()
-      else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt);
+      else future_result ctxt' (fork result) (Thm.term_of stmt);
   in
     Conjunction.elim_balanced (length props) res
     |> map (Assumption.export false ctxt' ctxt)
     |> Variable.export ctxt' ctxt
     |> map Drule.zero_var_indexes