diff -r 03eb7f7bb990 -r d8c99a497502 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] =