src/Pure/context.ML

--- a/src/Pure/context.ML	Sat Sep 04 21:45:43 2021 +0200
+++ b/src/Pure/context.ML	Sat Sep 04 22:05:35 2021 +0200
@@ -466,10 +466,10 @@
 end;
 
 fun theory_data_size thy =
-  (data_of thy, []) |-> Datatab.fold_rev (fn (k, _) =>
+  build (data_of thy |> Datatab.fold_rev (fn (k, _) =>
     (case Theory_Data.obj_size k thy of
       NONE => I
-    | SOME n => (cons (invoke_pos k, n))));
+    | SOME n => (cons (invoke_pos k, n)))));