# HG changeset patch
# User wenzelm
# Date 1708599149 -3600
# Node ID 48628d2e30ef54f2463244619d5ca97a6d9a28ad
# Parent  d2cb610c42291a9814b4e43cdc827420e8eb93f1
tuned names;

diff -r d2cb610c4229 -r 48628d2e30ef src/Pure/ML/ml_heap.scala
--- 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)
       }
     }