tuned -- slightly smaller future closure size;
authorwenzelm
Wed, 02 May 2018 23:34:40 +0200
changeset 68068 0acf3206a723
parent 68067 b91c4acc1aaf
child 68070 8dc792d440b9
tuned -- slightly smaller future closure size;
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') =