# HG changeset patch
# User wenzelm
# Date 1491572100 -7200
# Node ID 7689342a3097f5f26f3e07da6750efaf2ac05903
# Parent  a2500bb825944357bc6f3e46af79bf8a717843b5
tuned;

diff -r a2500bb82594 -r 7689342a3097 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Apr 07 13:52:06 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Apr 07 15:35:00 2017 +0200
@@ -27,6 +27,25 @@
 
     lazy val bootstrap: Base =
       Base(keywords = Thy_Header.bootstrap_header, syntax = Thy_Header.bootstrap_syntax)
+
+    private[Sessions] def known_theories(bases: Iterable[Base], names: Iterable[Document.Node.Name])
+      : Map[String, Document.Node.Name] =
+    {
+      val bases_iterator =
+        for { base <- bases.iterator; (_, name) <- base.known_theories.iterator }
+          yield name
+
+      (Map.empty[String, Document.Node.Name] /: (bases_iterator ++ names.iterator))({
+        case (known, name) =>
+          known.get(name.theory) match {
+            case Some(name1) if name != name1 =>
+              error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
+            case _ =>
+              known + (name.theory -> name) +
+                (Long_Name.base_name(name.theory) -> name)  // legacy
+          }
+        })
+    }
   }
 
   sealed case class Base(
@@ -91,25 +110,8 @@
           }
 
           val known_theories =
-          {
-            val imports_iterator =
-              for {
-                import_session <- info.imports.iterator
-                (_, name) <- sessions(import_session).known_theories.iterator
-              } yield name
-            val deps_iterator = thy_deps.deps.iterator.map(_.name)
-
-            (parent_base.known_theories /: (imports_iterator ++ deps_iterator))({
-              case (known, name) =>
-                known.get(name.theory) match {
-                  case Some(name1) if name != name1 =>
-                    error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
-                  case _ =>
-                    known + (name.theory -> name) +
-                      (Long_Name.base_name(name.theory) -> name)  // legacy
-                }
-              })
-          }
+            Base.known_theories(
+              parent_base :: info.imports.map(sessions(_)), thy_deps.deps.map(_.name))
 
           val loaded_theories = thy_deps.loaded_theories
           val keywords = thy_deps.keywords