more operations for profiling;

--- a/src/Pure/ML/ml_heap.ML	Thu Mar 30 16:04:02 2023 +0200
+++ b/src/Pure/ML/ml_heap.ML	Thu Mar 30 16:09:19 2023 +0200
@@ -8,6 +8,7 @@
 sig
   val obj_size: 'a -> int
   val sizeof1: 'a -> int
+  val sizeof_list: 'a list -> int
   val sizeof: 'a list -> int
   val full_gc: unit -> unit
   val gc_now: unit -> Time.time
@@ -21,7 +22,9 @@
 val obj_size = PolyML.objSize;
 
 fun sizeof1 x = obj_size x * ML_System.platform_obj_size;
-fun sizeof xs = (obj_size xs - 3 * length xs) * ML_System.platform_obj_size;
+
+fun sizeof_list xs = 3 * length xs * ML_System.platform_obj_size;
+fun sizeof xs = obj_size xs * ML_System.platform_obj_size - sizeof_list xs;
 
 val full_gc = PolyML.fullGC;