src/Pure/Thy/thy_info.scala

--- a/src/Pure/Thy/thy_info.scala	Mon Apr 03 16:50:44 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Mon Apr 03 17:00:36 2017 +0200
@@ -71,7 +71,7 @@
       val import_errors =
         (for {
           (theory, names) <- seen_names.iterator_list
-          if !resources.base.loaded_theories(theory)
+          if !resources.session_base.loaded_theories(theory)
           if names.length > 1
         } yield
           "Incoherent imports for theory " + quote(theory) + ":\n" +
@@ -83,10 +83,12 @@
     }
 
     lazy val syntax: Outer_Syntax =
-      resources.base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
+      resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
 
     def loaded_theories: Set[String] =
-      (resources.base.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
+      (resources.session_base.loaded_theories /: rev_deps) {
+        case (loaded, dep) => loaded + dep.name.theory
+      }
 
     def loaded_files: List[Path] =
     {
@@ -118,7 +120,7 @@
         required_by(initiators) + Position.here(require_pos)
 
     val required1 = required + thy
-    if (required.seen(name) || resources.base.loaded_theory(name)) required1
+    if (required.seen(name) || resources.session_base.loaded_theory(name)) required1
     else {
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))