future proofs: more robust check via Future.enabled;

--- a/src/Pure/Isar/skip_proof.ML	Thu Dec 11 22:53:50 2008 +0100
+++ b/src/Pure/Isar/skip_proof.ML	Fri Dec 12 12:14:02 2008 +0100
@@ -34,7 +34,7 @@
   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
 
 fun prove ctxt xs asms prop tac =
-  (if ! future_scheduler then Goal.prove_future else Goal.prove) ctxt xs asms prop
+  (if Future.enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
     (fn args => fn st =>
       if ! quick_and_dirty
       then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st

--- a/src/Pure/Thy/thy_info.ML	Thu Dec 11 22:53:50 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Dec 12 12:14:02 2008 +0100
@@ -375,7 +375,7 @@
     else if Multithreading.self_critical () then
      (warning (loader_msg "no multithreading within critical section" []);
       schedule_seq tasks)
-    else if ! future_scheduler then future_schedule tasks
+    else if Future.enabled () then future_schedule tasks
     else ignore (Exn.release_all (map Exn.Exn (Schedule.schedule (Int.min (m, n)) next_task tasks)))
   end;
 

--- a/src/Pure/goal.ML	Thu Dec 11 22:53:50 2008 +0100
+++ b/src/Pure/goal.ML	Fri Dec 12 12:14:02 2008 +0100
@@ -177,7 +177,8 @@
             else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
           end);
     val res =
-      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result ()
+      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (Future.enabled ())
+      then result ()
       else future_result ctxt' (Future.fork_background result) (Thm.term_of stmt);
   in
     Conjunction.elim_balanced (length props) res