--- 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)