src/Pure/Isar/proof.ML

--- a/src/Pure/Isar/proof.ML	Sun Jan 11 17:34:02 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Jan 11 18:18:35 2009 +0100
@@ -1041,7 +1041,7 @@
 local
 
 fun future_terminal_proof proof1 proof2 meths int state =
-  if int orelse is_relevant state orelse not (Future.enabled () andalso ! Goal.parallel_proofs)
+  if int orelse is_relevant state orelse not (Goal.future_enabled ())
   then proof1 meths state
   else snd (state |> proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))));