--- a/src/Pure/proofterm.ML Wed May 02 19:18:29 2018 +0200
+++ b/src/Pure/proofterm.ML Wed May 02 23:34:40 2018 +0200
@@ -1613,11 +1613,15 @@
val body0 =
if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
else
- (singleton o Future.cond_forks)
- {name = "Proofterm.prepare_thm_proof", group = NONE,
- deps = [], pri = 1, interrupts = true}
- (fn () =>
- make_body0 (shrink_proof (rew_proof thy (fold_rev implies_intr_proof hyps prf))));
+ let
+ val rew = rew_proof thy;
+ val prf' = fold_rev implies_intr_proof hyps prf;
+ in
+ (singleton o Future.cond_forks)
+ {name = "Proofterm.prepare_thm_proof", group = NONE,
+ deps = [], pri = 1, interrupts = true}
+ (fn () => make_body0 (shrink_proof (rew prf')))
+ end;
fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
val (i, body') =