author | wenzelm |

Wed May 02 23:34:40 2018 +0200 (21 months ago ago) | |

changeset 68069 | 0acf3206a723 |

parent 68068 | b91c4acc1aaf |

child 68070 | 8dc792d440b9 |

tuned -- slightly smaller future closure size;

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') =