--- a/src/Pure/Isar/skip_proof.ML Sat Jan 10 16:58:56 2009 +0100
+++ b/src/Pure/Isar/skip_proof.ML Sat Jan 10 21:32:30 2009 +0100
@@ -34,7 +34,8 @@
ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
fun prove ctxt xs asms prop tac =
- (if Future.enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
+ (if Future.enabled () andalso ! Goal.parallel_proofs 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