src/Pure/facts.ML

--- a/src/Pure/facts.ML	Sat Sep 04 21:45:43 2021 +0200
+++ b/src/Pure/facts.ML	Sat Sep 04 22:05:35 2021 +0200
@@ -217,7 +217,8 @@
 fun consolidate facts =
   let
     val unfinished =
-      (facts, []) |-> fold_static_lazy (fn (_, ths) => if Lazy.is_finished ths then I else cons ths);
+      build (facts |> fold_static_lazy (fn (_, ths) =>
+        if Lazy.is_finished ths then I else cons ths));
     val _ = Lazy.consolidate unfinished;
   in facts end;