--- a/src/Pure/ML/ml_heap.scala Fri Jun 23 13:47:34 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala Fri Jun 23 13:51:23 2023 +0200
@@ -66,10 +66,6 @@
val table = make_table("slices", List(name, slice, content))
}
- def known_entry(db: SQL.Database, name: String): Boolean =
- db.execute_query_statementB(
- Base.table.select(List(Base.name), sql = Base.name.where_equal(name)))
-
def get_entry(db: SQL.Database, name: String): Option[SHA1.Digest] =
db.execute_query_statementO[String](
Base.table.select(List(Base.digest), sql = Generic.name.where_equal(name)),