enable PARALLEL_GOALS more liberally, unlike forked proofs (cf. 34b9652b2f45);
authorwenzelm
Sat, 16 Apr 2011 23:38:25 +0200
changeset 42371 5900f06b4198
parent 42370 244911efd275
child 42372 6cca8d2a79ad
enable PARALLEL_GOALS more liberally, unlike forked proofs (cf. 34b9652b2f45);
src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Apr 16 22:21:34 2011 +0200
+++ b/src/Pure/goal.ML	Sat Apr 16 23:38:25 2011 +0200
@@ -347,7 +347,7 @@
 fun PARALLEL_GOALS tac =
   Thm.adjust_maxidx_thm ~1 #>
   (fn st =>
-    if not (future_enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1
+    if not (Multithreading.enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1
     then DETERM tac st
     else
       let