src/Pure/PIDE/resources.scala

        (sessions_structure.dest_session_directories,
        (sessions_structure.bibtex_entries,
        (command_timings,
        (Command_Span.load_commands.map(cmd => (cmd.name, cmd.position)),
        (Scala.functions,
-       (session_base.global_theories.toList,
+       (sessions_structure.global_theories.toList,
         session_base.loaded_theories.keys)))))))))
   }
 
 
   /* file formats */

       node_name = Document.Node.Name(path.implode, path.dir.implode, theory)
       file <- loaded_files(syntax, node_name, load_commands(syntax, node_name)())
     } yield file
   }
 
+  def global_theory(theory: String): Boolean =
+    sessions_structure.global_theories.isDefinedAt(theory)
+
   def theory_name(qualifier: String, theory: String): String =
-    if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory))
-      theory
+    if (Long_Name.is_qualified(theory) || global_theory(theory)) theory
     else Long_Name.qualify(qualifier, theory)
 
   def find_theory_node(theory: String): Option[Document.Node.Name] = {
     val thy_file = Path.basic(Long_Name.base_name(theory)).thy
     val session = sessions_structure.theory_qualifier(theory)

   def import_name(info: Sessions.Info, s: String): Document.Node.Name =
     import_name(info.name, info.dir.implode, s)
 
   def find_theory(file: JFile): Option[Document.Node.Name] = {
     for {
-      qualifier <- session_base.session_directories.get(File.canonical(file).getParentFile)
+      qualifier <- sessions_structure.session_directories.get(File.canonical(file).getParentFile)
       theory_base <- proper_string(Thy_Header.theory_name(file.getName))
       theory = theory_name(qualifier, theory_base)
       theory_node <- find_theory_node(theory)
       if File.eq(theory_node.path.file, file)
     } yield theory_node

       (session, (info, _))  <- sessions_structure.imports_graph.iterator
       dir <- (if (session == context_session) context_dir.toList else info.dirs).iterator
       theory <- Thy_Header.try_read_dir(dir).iterator
       if Completion.completed(s)(theory)
     } yield {
-      if (session == context_session || session_base.global_theories.isDefinedAt(theory)) theory
+      if (session == context_session || global_theory(theory)) theory
       else Long_Name.qualify(session, theory)
     }).toList.sorted
   }
 
   def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = {