# HG changeset patch
# User wenzelm
# Date 1659613797 -7200
# Node ID 72ffa12f9b2e7f6608aedd3ace03518df2de6dcd
# Parent  d0037f04bba0165963fe372b687265954b7a207f
tuned signature;

diff -r d0037f04bba0 -r 72ffa12f9b2e src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Thu Aug 04 13:44:21 2022 +0200
+++ b/src/Pure/Thy/export.scala	Thu Aug 04 13:49:57 2022 +0200
@@ -256,16 +256,15 @@
   /* abstract provider */
 
   object Provider {
-    def none: Provider =
+    val none: Provider =
       new Provider {
         def theory_names: List[String] = Nil
         def apply(export_name: String): Option[Entry] = None
         def focus(other_theory: String): Provider = this
-
         override def toString: String = "none"
       }
 
-    private def make_database(
+    private def database_provider(
         db: SQL.Database,
         cache: XML.Cache,
         session: String,
@@ -288,7 +287,7 @@
 
         def focus(other_theory: String): Provider =
           if (other_theory == theory) this
-          else make_database(db, cache, session, theory, _theory_names)
+          else database_provider(db, cache, session, theory, _theory_names)
 
         override def toString: String = db.toString
       }
@@ -299,7 +298,7 @@
       cache: XML.Cache,
       session: String,
       theory: String = ""
-    ): Provider = make_database(db, cache, session, theory, Synchronized(None))
+    ): Provider = database_provider(db, cache, session, theory, Synchronized(None))
 
     def snapshot(
       resources: Resources,