src/Pure/Build/store.scala

 
   def heap_shasum(database_server: Option[SQL.Database], name: String): SHA1.Shasum = {
     def get_database: Option[SHA1.Digest] = {
       for {
         db <- database_server
-        digest <- ML_Heap.get_entries(db, List(name)).valuesIterator.nextOption()
+        digest <- ML_Heap.read_digests(db, List(name)).valuesIterator.nextOption()
       } yield digest
     }
 
     get_database orElse get_session(name).heap_digest() match {
       case Some(digest) => SHA1.shasum(digest, name)