# HG changeset patch
# User wenzelm
# Date 1659625715 -7200
# Node ID 6f5fc43a3e454ca87b697de8715242ca0c000fce
# Parent  195f4289f905b7a983f3759ee9205f31d35cba0e
unused;

diff -r 195f4289f905 -r 6f5fc43a3e45 src/Pure/Thy/export.scala
--- 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,