src/Pure/Isar/skip_proof.ML
changeset 29435 a5f84ac14609
parent 29088 95a239a5e055
child 29448 34b9652b2f45
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Sat Jan 10 16:58:56 2009 +0100
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Sat Jan 10 21:32:30 2009 +0100
     1.3 @@ -34,7 +34,8 @@
     1.4    ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
     1.5  
     1.6  fun prove ctxt xs asms prop tac =
     1.7 -  (if Future.enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
     1.8 +  (if Future.enabled () andalso ! Goal.parallel_proofs then Goal.prove_future else Goal.prove)
     1.9 +    ctxt xs asms prop
    1.10      (fn args => fn st =>
    1.11        if ! quick_and_dirty
    1.12        then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st