--- 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;