# HG changeset patch
# User wenzelm
# Date 1302989905 -7200
# Node ID 5900f06b41986deb84723de3039aafbdb63af09b
# Parent  244911efd2750dffacffa462fe8b9db6f3597f6f
enable PARALLEL_GOALS more liberally, unlike forked proofs (cf. 34b9652b2f45);

diff -r 244911efd275 -r 5900f06b4198 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