--- a/src/Pure/Thy/export.scala Thu Aug 04 14:48:05 2022 +0200
+++ b/src/Pure/Thy/export.scala Thu Aug 04 17:08:35 2022 +0200
@@ -256,14 +256,6 @@
/* abstract provider */
object Provider {
- val none: Provider =
- new Provider {
- override def theory_names: List[String] = Nil
- override def apply(export_name: String): Option[Entry] = None
- override def focus(other_theory: String): Provider = this
- override def toString: String = "none"
- }
-
private def database_provider(
db: SQL.Database,
cache: XML.Cache,