diff --git a/tools/afp_structure.scala b/tools/afp_structure.scala
--- a/tools/afp_structure.scala
+++ b/tools/afp_structure.scala
@@ -1,130 +1,126 @@
 /* Author: Fabian Huch, TU Muenchen
 
 AFP Metadata file structure with save and load operations.
  */
 package afp
 
 
 import isabelle.*
 
 
 class AFP_Structure private(val base_dir: Path) {
   /* files */
 
   val metadata_dir = base_dir + Path.basic("metadata")
-
-  val thys_dir = base_dir + Path.basic("thys")
+  val thys_dir = AFP.main_dir(base_dir)
 
   def entry_thy_dir(name: Metadata.Entry.Name): Path = thys_dir + Path.basic(name)
 
   val authors_file = metadata_dir + Path.basic("authors.toml")
-
   val releases_file = metadata_dir + Path.basic("releases.toml")
-  
   val licenses_file = metadata_dir + Path.basic("licenses.toml")
-
   val topics_file = metadata_dir + Path.basic("topics.toml")
 
   val entries_dir = metadata_dir + Path.basic("entries")
 
   def entry_file(name: Metadata.Entry.Name): Path = entries_dir + Path.basic(name + ".toml")
 
 
   /* load */
 
   private def load[A](file: Path, parser: isabelle.TOML.Table => A): A = {
     val content = File.read(file)
     val toml =
       try { TOML.parse(content) }
       catch { case ERROR(msg) => error("Could not parse " + file.toString + ": " + msg) }
     parser(toml)
   }
 
   def load_authors: List[Metadata.Author] = load(authors_file, Metadata.TOML.to_authors)
 
   def load_releases: List[Metadata.Release] = load(releases_file, Metadata.TOML.to_releases)
 
   def load_licenses: List[Metadata.License] = load(licenses_file, Metadata.TOML.to_licenses)
-  
+
   def load_topics: List[Metadata.Topic] = load(topics_file, Metadata.TOML.to_topics)
 
   def load_entry(name: Metadata.Entry.Name,
     authors: Map[Metadata.Author.ID, Metadata.Author],
     topics: Map[Metadata.Topic.ID, Metadata.Topic],
     licenses: Map[Metadata.License.ID, Metadata.License],
     releases: Map[Metadata.Entry.Name, List[Metadata.Release]]
   ): Metadata.Entry = {
     val entry_releases = releases.getOrElse(name, Nil)
     load(entry_file(name), toml =>
       Metadata.TOML.to_entry(name, toml, authors, topics, licenses, entry_releases))
   }
 
   def load(): List[Metadata.Entry] = {
     val authors = load_authors.map(author => author.id -> author).toMap
     val topics = Utils.grouped_sorted(load_topics.flatMap(_.all_topics), (t: Metadata.Topic) => t.id)
     val licenses = load_licenses.map(license => license.id -> license).toMap
     val releases = load_releases.groupBy(_.entry)
     entries.map(name => load_entry(name, authors, topics, licenses, releases))
   }
 
 
   /* save */
 
   private def save(file: Path, content: isabelle.TOML.Table): Unit = {
     file.dir.file.mkdirs()
     File.write(file, TOML.Format(content))
   }
 
   def save_authors(authors: List[Metadata.Author]): Unit =
     save(authors_file, Metadata.TOML.from_authors(authors))
 
   def save_releases(releases: List[Metadata.Release]): Unit =
     save(releases_file, Metadata.TOML.from_releases(releases))
 
   def save_topics(topics: List[Metadata.Topic]): Unit =
     save(topics_file, Metadata.TOML.from_topics(topics))
 
   def save_entry(entry: Metadata.Entry): Unit =
     save(entry_file(entry.name), Metadata.TOML.from_entry(entry))
 
 
   /* sessions */
 
   def entries_unchecked: List[Metadata.Entry.Name] = {
     val Entry = """([a-zA-Z0-9+_-]+)\.toml""".r
     File.read_dir(entries_dir).map {
       case Entry(name) => name
       case f => error("Unrecognized file in metadata: " + f)
     }
   }
-  
+
   def entries: List[Metadata.Entry.Name] = {
     val session_entries = Sessions.parse_roots(thys_dir + Path.basic("ROOTS"))
 
     val session_set = session_entries.toSet
     val metadata_set = entries_unchecked.toSet
 
     if (session_set != metadata_set) {
       val inter = session_set.intersect(metadata_set)
       val session_without_metadata =
         if (session_set.subsetOf(inter)) ""
         else "No metadata for session in ROOTS: " + commas_quote(session_set -- inter)
       val metadata_without_session =
         if (metadata_set.subsetOf(inter)) ""
         else "Metadata entries missing in ROOTS: " + commas_quote(metadata_set -- inter)
       error("Metadata does not match sessions:\n" + session_without_metadata + metadata_without_session)
     } else session_entries
   }
 
   def sessions_structure: Sessions.Structure =
     Sessions.load_structure(options = Options.init(), select_dirs = List(thys_dir))
 
   def entry_sessions(name: Metadata.Entry.Name): List[Sessions.Session_Entry] =
     Sessions.parse_root(thys_dir + Path.make(List(name, "ROOT"))).collect { case e: Sessions.Session_Entry => e }
 
   def hg_id: String = Mercurial.repository(base_dir).id()
 }
 
 object AFP_Structure {
-  def apply(base_dir: Path = Path.explode("$AFP_BASE")): AFP_Structure = new AFP_Structure(base_dir.absolute)
+  def apply(base_dir: Path = AFP.BASE): AFP_Structure = new AFP_Structure(base_dir.absolute)
 }