src/Pure/goal.ML

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

       |> Thm.instantiate (instT, [])
       |> Drule.forall_elim_list fixes
       |> fold (Thm.elim_implies o Thm.assume) assms;
   in local_result end;
 
+val parallel_proofs = ref true;
+
 
 
 (** tactical theorem proving **)
 
 (* prove_internal -- minimal checks, no normalization of result! *)

             if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res]
             then Thm.check_shyps sorts res
             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 ())
+      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse
+        not (Future.enabled () andalso ! parallel_proofs)
       then result ()
       else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt);
   in
     Conjunction.elim_balanced (length props) res
     |> map (Assumption.export false ctxt' ctxt)