# HG changeset patch
# User wenzelm
# Date 1231245402 -3600
# Node ID cea7b4034461dd86aab943b2882ee542fa0b42cf
# Parent  c1f024b4d76d4297690e0be6c585f75f110a34aa
future_terminal_proof: check Future.enabled;

diff -r c1f024b4d76d -r cea7b4034461 src/Pure/Isar/proof.ML
--- 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'))));