diff -r 1c3d0c12bb51 -r 9f2de457b95e src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Oct 31 17:56:28 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 18:45:33 2017 +0100
@@ -321,12 +321,6 @@
 
   /* base info */
 
-  sealed case class Base_Info(base: Base, errors: List[String])
-  {
-    def platform_path: Base_Info = copy(base = base.platform_path)
-    def check: Base = if (errors.isEmpty) base else error(cat_lines(errors))
-  }
-
   def session_base_info(
     options: Options,
     session: String,
@@ -338,13 +332,19 @@
     val global_theories = full_sessions.global_theories
     val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
 
-    val deps =
-      Sessions.deps(if (all_known) full_sessions else selected_sessions,
-        global_theories, inlined_files = inlined_files)
-
+    val sessions: T = if (all_known) full_sessions else selected_sessions
+    val deps = Sessions.deps(sessions, global_theories, inlined_files = inlined_files)
     val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
 
-    Base_Info(base, deps.errors)
+    new Base_Info(sessions, deps, base)
+  }
+
+  final class Base_Info private [Sessions](val sessions: T, val deps: Deps, val base: Base)
+  {
+    def platform_path: Base_Info = new Base_Info(sessions, deps, base.platform_path)
+
+    def errors: List[String] = deps.errors
+    def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
   }