--- a/src/Pure/proofterm.ML Wed Jul 17 23:51:10 2013 +0200
+++ b/src/Pure/proofterm.ML Thu Jul 18 13:12:54 2013 +0200
@@ -1491,7 +1491,6 @@
postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body));
in
if null promises then Future.map postproc body
- else if Context.is_draft thy then Future.value (fulfill ())
else if Future.is_finished body andalso length promises = 1 then
Future.map (fn _ => fulfill ()) (snd (hd promises))
else
@@ -1546,18 +1545,16 @@
(Type.strip_sorts o atyp_map) args;
val argsP = map OfClass outer_constraints @ map Hyp hyps;
- fun full_proof0 () =
- #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)));
-
fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
val body0 =
if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
- else if Context.is_draft thy then Future.value (make_body0 (full_proof0 ()))
else
(singleton o Future.cond_forks)
{name = "Proofterm.prepare_thm_proof", group = NONE,
deps = [], pri = 0, interrupts = true}
- (make_body0 o full_proof0);
+ (fn () =>
+ make_body0
+ (#4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))));
fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
val (i, body') =