summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 02 May 2018 23:34:40 +0200 | |

changeset 68068 | 0acf3206a723 |

parent 68067 | b91c4acc1aaf |

child 68070 | 8dc792d440b9 |

tuned -- slightly smaller future closure size;

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