src/Pure/Thy/sessions.scala

 
     val selected_sessions1 =
     {
       val sel_sessions1 = session1 :: session :: include_sessions
       val select_sessions1 =
-        if (session_focus) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1
+        if (session_focus) {
+          full_sessions1.check_sessions(sel_sessions1)
+          full_sessions1.imports_descendants(sel_sessions1)
+        }
+        else sel_sessions1
       full_sessions1.selection(Selection(sessions = select_sessions1))
     }
 
     val sessions1 = if (all_known) full_sessions1 else selected_sessions1
     val deps1 = Sessions.deps(sessions1, global_theories, progress = progress)

                   error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
                 case _ => global + (thy -> qualifier)
               }
           })
 
-    def selection(sel: Selection): Structure =
-    {
-      val bad_sessions =
-        SortedSet((sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions).
-          filterNot(defined(_)): _*).toList
+    def check_sessions(names: List[String])
+    {
+      val bad_sessions = SortedSet(names.filterNot(defined(_)): _*).toList
       if (bad_sessions.nonEmpty)
         error("Undefined session(s): " + commas_quote(bad_sessions))
+    }
+
+    def selection(sel: Selection): Structure =
+    {
+      check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
 
       val excluded = sel.excluded(build_graph).toSet
 
       def restrict(graph: Graph[String, Info]): Graph[String, Info] =
       {