# HG changeset patch
# User wenzelm
# Date 1525296880 -7200
# Node ID 0acf3206a723993fac5d9487bcd68f3f45bb06b5
# Parent  b91c4acc1aaf8b7d3857ca194c60bb84e99c1ca5
tuned -- slightly smaller future closure size;

diff -r b91c4acc1aaf -r 0acf3206a723 src/Pure/proofterm.ML
--- 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') =