--- a/src/Pure/goal.ML Sat Jan 10 16:58:56 2009 +0100
+++ b/src/Pure/goal.ML Sat Jan 10 21:32:30 2009 +0100
@@ -6,6 +6,7 @@
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
@@ -123,6 +124,8 @@
|> fold (Thm.elim_implies o Thm.assume) assms;
in local_result end;
+val parallel_proofs = ref true;
+
(** tactical theorem proving **)
@@ -172,7 +175,8 @@
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