# HG changeset patch
# User wenzelm
# Date 1687521083 -7200
# Node ID 7ba63bd216afb97b0e8edc9c38943c75c834d883
# Parent  140a6f2e3728c6776d640bc9d62aa6bbe5386f97
unused;

diff -r 140a6f2e3728 -r 7ba63bd216af src/Pure/ML/ml_heap.scala
--- 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)),