src/Pure/Thy/sessions.scala

       val bad_sessions = SortedSet(names.filterNot(defined(_)): _*).toList
       if (bad_sessions.nonEmpty)
         error("Undefined session(s): " + commas_quote(bad_sessions))
     }
 
+    def check_sessions(sel: Selection): Unit =
+      check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
+
     private def selected(graph: Graph[String, Info], sel: Selection): List[String] =
     {
+      check_sessions(sel)
+
       val select_group = sel.session_groups.toSet
       val select_session = sel.sessions.toSet ++ graph.all_succs(sel.base_sessions)
 
       val selected0 =
         if (sel.all_sessions) graph.keys

       else selected0
     }
 
     def selection(sel: Selection): Structure =
     {
-      check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
+      check_sessions(sel)
 
       val excluded =
       {
         val exclude_group = sel.exclude_session_groups.toSet
         val exclude_group_sessions =