src/Pure/facts.ML

   Name_Space.fold_table (fn (a, Static ths) => f (a, ths) | _ => I) o facts_of;
 
 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;
 
 fun included verbose prev_facts facts name =
   not (exists (fn prev => defined prev name) prev_facts orelse