src/Pure/Tools/profiling.scala

     global_thms: Int = 0,
     sizeof_thys_id: Space = Space.zero,
     sizeof_thms_id: Space = Space.zero,
     sizeof_terms: Space = Space.zero,
     sizeof_types: Space = Space.zero,
+    sizeof_names: Space = Space.zero,
     sizeof_spaces: Space = Space.zero)
 
   object Statistics {
     private val encode_args: XML.Encode.T[List[String]] =
       (args: List[String]) =>
         { import XML.Encode._; list(string)(args) }
 
     private val decode_result: XML.Decode.T[Session_Statistics] =
       (body: XML.Body) =>
         {
-          val (a, (b, (c, (d, (e, (f, (g, (h, (i, j))))))))) = {
+          val (a, (b, (c, (d, (e, (f, (g, (h, (i, (j, k)))))))))) = {
             import XML.Decode._
             pair(int, pair(int, pair(int, pair(int, pair(int,
-              pair(long, pair(long, pair(long, pair(long, long)))))))))(body)
+              pair(long, pair(long, pair(long, pair(long, pair(long, long))))))))))(body)
           }
           Session_Statistics(
             theories = a,
             garbage_theories = b,
             locales = c,

             global_thms = e,
             sizeof_thys_id = Space.bytes(f),
             sizeof_thms_id = Space.bytes(g),
             sizeof_terms = Space.bytes(h),
             sizeof_types = Space.bytes(i),
-            sizeof_spaces = Space.bytes(j))
+            sizeof_names = Space.bytes(j),
+            sizeof_spaces = Space.bytes(k))
         }
 
     def make(
       store: Store,
       session_background: Sessions.Background,

         heap_size = File.space(store.the_heap(session_name)),
         thys_id_size = session.sizeof_thys_id,
         thms_id_size = session.sizeof_thms_id,
         terms_size = session.sizeof_terms,
         types_size = session.sizeof_types,
+        names_size = session.sizeof_names,
         spaces_size = session.sizeof_spaces)
     }
 
     val empty: Statistics = new Statistics()
 

         "heap_size",
         "thys_id_size%",
         "thms_id_size%",
         "terms_size%",
         "types_size%",
+        "names_size%",
         "spaces_size%")
 
     def header: List[String] =
       "session" :: header0.flatMap(a => List(a, "\u2211" + a))
   }

     val heap_size: Space = Space.zero,
     val thys_id_size: Space = Space.zero,
     val thms_id_size: Space = Space.zero,
     val terms_size: Space = Space.zero,
     val types_size: Space = Space.zero,
+    val names_size: Space = Space.zero,
     val spaces_size: Space = Space.zero
   ) {
     private def print_total_theories: String =
       if (theories == 0) "0"
       else {

         heap_size.print,
         size_percentage(thys_id_size).toString,
         size_percentage(thms_id_size).toString,
         size_percentage(terms_size).toString,
         size_percentage(types_size).toString,
+        size_percentage(names_size).toString,
         size_percentage(spaces_size).toString)
 
     def fields: List[Any] =
       session :: fields0.zipWithIndex.flatMap({ case (a, i) => List(a, cumulative.fields0(i)) })
 

             heap_size = other.cumulative.heap_size + heap_size,
             thys_id_size = other.cumulative.thys_id_size + thys_id_size,
             thms_id_size = other.cumulative.thms_id_size + thms_id_size,
             terms_size = other.cumulative.terms_size + terms_size,
             types_size = other.cumulative.types_size + types_size,
+            names_size = other.cumulative.names_size + names_size,
             spaces_size = other.cumulative.spaces_size + spaces_size)
       }
 
     override def toString: String = "Statistics(" + session + ")"
   }