--- 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