future_terminal_proof: check Future.enabled;

--- a/src/Pure/Isar/proof.ML	Tue Jan 06 08:50:12 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Jan 06 13:36:42 2009 +0100
@@ -1029,7 +1029,7 @@
 end;
 
 fun future_terminal_proof meths state =
-  if is_relevant state then global_terminal_proof meths state
+  if is_relevant state orelse not (Future.enabled ()) then global_terminal_proof meths state
   else #2 (state |> future_proof (fn state' =>
     Future.fork_pri ~1 (fn () => ((), global_terminal_proof meths state'))));