# HG changeset patch
# User wenzelm
# Date 1520440077 -3600
# Node ID a25f9076a0b3cf93a2ec7b4f7829d9155fd00408
# Parent  2d3c1091527b8adf2ea7c2d89f336e9f8b296216
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;

diff -r 2d3c1091527b -r a25f9076a0b3 src/Pure/more_thm.ML
--- 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;