# HG changeset patch
# User wenzelm
# Date 1510049497 -3600
# Node ID f6aa133f9b16e30260618af9b78490b02ecd8d6f
# Parent  ce64546693603509d1033eea76d0c36e4871964a
backed out odd "bug fix" 671decd2e627;

diff -r ce6454669360 -r f6aa133f9b16 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Tue Nov 07 10:22:10 2017 +0100
+++ b/src/Pure/General/graph.scala	Tue Nov 07 11:11:37 2017 +0100
@@ -70,7 +70,6 @@
 
   def keys_iterator: Iterator[Key] = iterator.map(_._1)
   def keys: List[Key] = keys_iterator.toList
-  def keys_set: Set[Key] = rep.keySet
 
   def dest: List[((Key, A), List[Key])] =
     (for ((x, (i, (_, succs))) <- iterator) yield ((x, i), succs.toList)).toList
diff -r ce6454669360 -r f6aa133f9b16 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Nov 07 10:22:10 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 11:11:37 2017 +0100
@@ -615,8 +615,8 @@
 
     def selection(select: Selection): (List[String], T) =
     {
+      val (_, build_graph1) = select(build_graph)
       val (selected, imports_graph1) = select(imports_graph)
-      val build_graph1 = build_graph.restrict(imports_graph1.keys_set)
       (selected, new T(build_graph1, imports_graph1))
     }