src/Pure/ML/ml_heap.scala

--- a/src/Pure/ML/ml_heap.scala	Fri Jul 07 18:04:45 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala	Sat Jul 08 13:13:10 2023 +0200
@@ -55,7 +55,7 @@
       val size = SQL.Column.long("size")
       val digest = SQL.Column.string("digest")
 
-      val table = make_table("", List(name, size, digest))
+      val table = make_table(List(name, size, digest))
     }
 
     object Slices {
@@ -63,7 +63,7 @@
       val slice = SQL.Column.int("slice").make_primary_key
       val content = SQL.Column.bytes("content")
 
-      val table = make_table("slices", List(name, slice, content))
+      val table = make_table(List(name, slice, content), name = "slices")
     }
 
     def get_entry(db: SQL.Database, name: String): Option[SHA1.Digest] =