tuned -- slightly smaller future closure size;
authorwenzelm
Wed May 02 23:34:40 2018 +0200 (21 months ago ago)
changeset 680690acf3206a723
parent 68068 b91c4acc1aaf
child 68070 8dc792d440b9
tuned -- slightly smaller future closure size;
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/proofterm.ML	Wed May 02 19:18:29 2018 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Wed May 02 23:34:40 2018 +0200
     1.3 @@ -1613,11 +1613,15 @@
     1.4      val body0 =
     1.5        if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
     1.6        else
     1.7 -        (singleton o Future.cond_forks)
     1.8 -          {name = "Proofterm.prepare_thm_proof", group = NONE,
     1.9 -            deps = [], pri = 1, interrupts = true}
    1.10 -          (fn () =>
    1.11 -            make_body0 (shrink_proof (rew_proof thy (fold_rev implies_intr_proof hyps prf))));
    1.12 +        let
    1.13 +          val rew = rew_proof thy;
    1.14 +          val prf' = fold_rev implies_intr_proof hyps prf;
    1.15 +        in
    1.16 +          (singleton o Future.cond_forks)
    1.17 +            {name = "Proofterm.prepare_thm_proof", group = NONE,
    1.18 +              deps = [], pri = 1, interrupts = true}
    1.19 +            (fn () => make_body0 (shrink_proof (rew prf')))
    1.20 +        end;
    1.21  
    1.22      fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
    1.23      val (i, body') =