src/Pure/ML/ml_heap.scala
changeset 79683 ade429ddb1fc
parent 79682 1fa1b32b0379
child 79685 45af93b0370a
--- a/src/Pure/ML/ml_heap.scala	Wed Feb 21 19:36:53 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala	Wed Feb 21 19:54:17 2024 +0100
@@ -72,8 +72,8 @@
 
     object Slices_Size {
       val name = Generic.name
-      val slice = SQL.Column.int("slice").make_primary_key
-      val size = SQL.Column.long("size")
+      val slice = Slices.slice
+      val size = SQL.Column.string("size")
 
       val table = make_table(List(name, slice, size),
         body = "SELECT name, slice, pg_size_pretty(length(content)::bigint) as size FROM " +