# HG changeset patch
# User wenzelm
# Date 1659710406 -7200
# Node ID b10c3d9dd48a411db2df7d25c847e64689bb5da8
# Parent  07e097f60b850603634fb6d88ebd4508068a9148
redundant;

diff -r 07e097f60b85 -r b10c3d9dd48a src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Aug 05 14:44:47 2022 +0200
+++ b/src/Pure/Thy/export.scala	Fri Aug 05 16:40:06 2022 +0200
@@ -341,8 +341,6 @@
   def open_context(store: Sessions.Store): Context =
     new Context(store.open_database_context()) { override def close(): Unit = db_context.close() }
 
-  def open_context(options: Options): Context = open_context(Sessions.store(options))
-
   class Session_Database private[Export](val session: String, val db: SQL.Database) {
     def close(): Unit = ()
   }