src/Pure/context.ML

   val proper_subthy: theory * theory -> bool
   val subthy_id: theory_id * theory_id -> bool
   val subthy: theory * theory -> bool
   val finish_thy: theory -> theory
   val begin_thy: string -> theory list -> theory
+  val theory_data_size: theory -> (Position.T * int) list
   (*proof context*)
   val raw_transfer: theory -> Proof.context -> Proof.context
   (*certificate*)
   datatype certificate = Certificate of theory | Certificate_Id of theory_id
   val certificate_theory: certificate -> theory

       else f kind x
   | NONE => raise Fail "Invalid theory data identifier");
 
 in
 
+fun invoke_pos k = invoke "" (K o #pos) k ();
 fun invoke_empty k = invoke "" (K o #empty) k ();
 val invoke_extend = invoke "extend" #extend;
 fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys);
 
 fun declare_theory_data pos empty extend merge =

     SOME x => x
   | NONE => invoke_empty k) |> dest;
 
 fun put k mk x = update_thy (Datatab.update (k, mk x));
 
-end;
+fun obj_size k thy =
+  Datatab.lookup (data_of thy) k |> Option.map ML_Heap.obj_size;
+
+end;
+
+fun theory_data_size thy =
+  (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))));
 
 
 
 (*** proof context ***)