src/Pure/goal.ML

 Goals in tactical theorem proving.
 *)
 
 signature BASIC_GOAL =
 sig
-  val parallel_proofs: bool ref
+  val parallel_proofs: int ref
   val SELECT_GOAL: tactic -> int -> tactic
   val CONJUNCTS: tactic -> int -> tactic
   val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
 end;
 

   val protect: thm -> thm
   val conclude: thm -> thm
   val finish: thm -> thm
   val norm_result: thm -> thm
   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
   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 ->

   #> Drule.zero_var_indexes;
 
 
 (* future_enabled *)
 
-val parallel_proofs = ref true;
+val parallel_proofs = ref 1;
 
 fun future_enabled () =
-  Future.enabled () andalso ! parallel_proofs andalso Future.is_worker ();
+  Future.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
+
+fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;
 
 
 (* future_result *)
 
 fun future_result ctxt result prop =