diff -r a041d49736f2 -r 1a69d3a3e3aa src/Pure/Tools/profiling.scala
--- a/src/Pure/Tools/profiling.scala	Thu Jul 13 13:10:40 2023 +0200
+++ b/src/Pure/Tools/profiling.scala	Thu Jul 13 13:51:08 2023 +0200
@@ -119,7 +119,8 @@
         "types_size%",
         "spaces_size%")
 
-    def header: List[String] = "session" :: header0 ::: header0.map(_ + "_cumulative")
+    def header: List[String] =
+      "session" :: header0.flatMap(a => List(a, "\u2211" + a))
   }
 
   final class Statistics private(
@@ -142,7 +143,7 @@
     private def thms_percentage(thms: Int): Percentage =
       percentage(thms, locale_thms + global_thms)
 
-    def fields0: List[Any] =
+    val fields0: List[Any] =
       List(
         theories,
         locales,
@@ -157,7 +158,8 @@
         size_percentage(types_size).toString,
         size_percentage(spaces_size).toString)
 
-    def fields: List[Any] = session :: fields0 ::: cumulative.fields0
+    def fields: List[Any] =
+      session :: fields0.zipWithIndex.flatMap({ case (a, i) => List(a, cumulative.fields0(i)) })
 
     lazy val cumulative: Statistics =
       parent match {