tuned names;

--- a/src/Pure/ML/ml_heap.scala	Wed Feb 21 20:37:53 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala	Thu Feb 22 11:52:29 2024 +0100
@@ -62,7 +62,7 @@
       val table = make_table(List(name, size, digest, uuid, log_db))
     }
 
-    object Base_Size {
+    object Size {
       val name = Generic.name
       val heap_size = SQL.Column.string("heap_size")
       val log_db_size = SQL.Column.string("log_db_size")
@@ -139,7 +139,7 @@
       for (table <- List(Base.table, Slices.table)) {
         db.execute_statement(table.delete(sql = Base.name.where_equal(name)))
       }
-      for (table <- List(Base_Size.table, Slices_Size.table)) {
+      for (table <- List(Size.table, Slices_Size.table)) {
         db.create_view(table)
       }
     }