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

author | wenzelm |

Wed, 07 Mar 2018 17:27:57 +0100 | |

changeset 67778 | a25f9076a0b3 |

parent 67777 | 2d3c1091527b |

child 67779 | fd2558014196 |

eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;

--- a/src/Pure/more_thm.ML Tue Mar 06 22:59:00 2018 +0100 +++ b/src/Pure/more_thm.ML Wed Mar 07 17:27:57 2018 +0100 @@ -677,11 +677,9 @@ (Proofs.map o cons) (Lazy.map_finished (map Thm.trim_context) ths); fun consolidate_theory thy = - let - val proofs = Proofs.get thy; - val pending = fold (fn ths => if Lazy.is_pending ths then cons ths else I) [] proofs; - val _ = Lazy.consolidate pending; - in Thm.consolidate (maps (map (Thm.transfer thy) o Lazy.force) (rev proofs)) end; + rev (Proofs.get thy) + |> maps (map (Thm.transfer thy) o Lazy.force) + |> Thm.consolidate;