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;