--- a/src/Pure/goal.ML Mon Apr 23 21:57:15 2018 +0100
+++ b/src/Pure/goal.ML Tue Apr 24 11:03:51 2018 +0200
@@ -7,7 +7,6 @@
signature BASIC_GOAL =
sig
val quick_and_dirty: bool Config.T
- val parallel_proofs: int Unsynchronized.ref
val SELECT_GOAL: tactic -> int -> tactic
val PREFER_GOAL: tactic -> int -> tactic
val CONJUNCTS: tactic -> int -> tactic
@@ -112,10 +111,8 @@
else skip
end;
-val parallel_proofs = Unsynchronized.ref 1;
-
fun future_enabled n =
- Multithreading.enabled () andalso ! parallel_proofs >= n andalso
+ Multithreading.parallel_proofs_enabled n andalso
is_some (Future.worker_task ());
fun future_enabled_timing t =