diff -r 5887ae5b95a8 -r 148891036469 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Sep 30 22:55:23 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Sun Oct 01 12:28:52 2017 +0200
@@ -373,14 +373,14 @@
     session_groups: List[String] = Nil,
     sessions: List[String] = Nil)
   {
-    def + (other: Selection): Selection =
+    def ++ (other: Selection): Selection =
       Selection(
         requirements = requirements || other.requirements,
         all_sessions = all_sessions || other.all_sessions,
-        exclude_session_groups = exclude_session_groups ::: other.exclude_session_groups,
-        exclude_sessions = exclude_sessions ::: other.exclude_sessions,
-        session_groups = session_groups ::: other.session_groups,
-        sessions = sessions ::: other.sessions)
+        exclude_session_groups = Library.merge(exclude_session_groups, other.exclude_session_groups),
+        exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions),
+        session_groups = Library.merge(session_groups, other.session_groups),
+        sessions = Library.merge(sessions, other.sessions))
 
     def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) =
     {