# HG changeset patch
# User wenzelm
# Date 1492452740 -7200
# Node ID ca8dcb2a500c2e64e50e3a488767e33cfb612044
# Parent  60d4fbed2b1f41b05418efe8bdb7befa20102b7d
proper imports_base, notably for thy_deps;

diff -r 60d4fbed2b1f -r ca8dcb2a500c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Apr 17 19:44:13 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Apr 17 20:12:20 2017 +0200
@@ -143,12 +143,16 @@
           if (progress.stopped) throw Exn.Interrupt()
 
           try {
-            val parent_base =
+            val parent_base: Sessions.Base =
               info.parent match {
                 case None => Base.bootstrap(global_theories)
                 case Some(parent) => session_bases(parent)
               }
-            val resources = new Resources(parent_base,
+            val imports_base: Sessions.Base =
+              parent_base.copy(known =
+                Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil))
+
+            val resources = new Resources(imports_base,
               default_qualifier = info.theory_qualifier(session_name))
 
             if (verbose || list_files) {
@@ -173,11 +177,6 @@
               }
             }
 
-            val known =
-              Known.make(info.dir,
-                parent_base :: info.imports.map(session_bases(_)),
-                thy_deps.deps.map(_.name))
-
             val syntax = thy_deps.syntax
 
             val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
@@ -210,11 +209,11 @@
             val base =
               Base(global_theories = global_theories,
                 loaded_theories = thy_deps.loaded_theories,
-                known = known,
+                known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
                 keywords = thy_deps.keywords,
                 syntax = syntax,
                 sources = all_files.map(p => (p, SHA1.digest(p.file))),
-                session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base))
+                session_graph = thy_deps.session_graph(info.parent getOrElse "", imports_base))
 
             session_bases + (session_name -> base)
           }
@@ -225,11 +224,9 @@
           }
       })
 
-    val known =
+    Deps(session_bases,
       if (all_known) Known.make(Path.current, session_bases.toList.map(_._2), Nil)
-      else Known.empty
-
-    Deps(session_bases, known)
+      else Known.empty)
   }
 
   def session_base(