minor performance tuning;

--- a/src/Pure/ML/ml_heap.scala	Thu Feb 22 19:58:52 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala	Thu Feb 22 20:05:24 2024 +0100
@@ -88,16 +88,18 @@
         name = "slices_size")
     }
 
-    def read_digests(db: SQL.Database, names: Iterable[String]): Map[String, SHA1.Digest] = {
-      db.execute_query_statement(
-        Base.table.select(List(Base.name, Base.heap_digest),
-          sql = Generic.name.where_member(names)),
-        List.from[(String, String)],
-        res => res.string(Base.name) -> res.string(Base.heap_digest)
-      ).collect({
-        case (name, digest) if digest.nonEmpty => name -> SHA1.fake_digest(digest)
-      }).toMap
-    }
+    def read_digests(db: SQL.Database, names: Iterable[String]): Map[String, SHA1.Digest] =
+      if (names.isEmpty) Map.empty
+      else {
+        db.execute_query_statement(
+          Base.table.select(List(Base.name, Base.heap_digest),
+            sql = Generic.name.where_member(names)),
+          List.from[(String, String)],
+          res => res.string(Base.name) -> res.string(Base.heap_digest)
+        ).collect({
+          case (name, digest) if digest.nonEmpty => name -> SHA1.fake_digest(digest)
+        }).toMap
+      }
 
     def read_slices(db: SQL.Database, name: String): List[Bytes] =
       db.execute_query_statement(