# HG changeset patch
# User wenzelm
# Date 1659868635 -7200
# Node ID 0132026e26eb0f57d0658283760092b27b45c112
# Parent  f9fcf06aa2ebdea943753da276c069c17c23fb5e
tuned signature;

diff -r f9fcf06aa2eb -r 0132026e26eb src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sun Aug 07 12:30:09 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sun Aug 07 12:37:15 2022 +0200
@@ -247,8 +247,8 @@
   extends AutoCloseable {
     def close(): Unit = ()
 
-    lazy val theory_names: List[String] = read_theory_names(db, session)
-    lazy val entry_names: List[Entry_Name] = read_entry_names(db, session)
+    lazy private [Export] val theory_names: List[String] = read_theory_names(db, session)
+    lazy private [Export] val entry_names: List[Entry_Name] = read_entry_names(db, session)
   }
 
   def open_database_context(store: Sessions.Store): Database_Context = {