# HG changeset patch
# User wenzelm
# Date 1657539610 -7200
# Node ID eb7480f29adc3758e4e669965ab3c67c5b2f8553
# Parent  88598f7c961439f17e501807de70ae1a19d87e7e
unused;

diff -r 88598f7c9614 -r eb7480f29adc src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Mon Jul 11 13:36:08 2022 +0200
+++ b/src/Pure/Thy/export.scala	Mon Jul 11 13:40:10 2022 +0200
@@ -83,12 +83,6 @@
     }
   }
 
-  def read_names(db: SQL.Database, session_name: String, theory_name: String): List[String] = {
-    val select = Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name))
-    db.using_statement(select)(stmt =>
-      stmt.execute_query().iterator(res => res.string(Data.name)).toList)
-  }
-
   def read_theory_names(db: SQL.Database, session_name: String): List[String] = {
     val select =
       Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true)