src/Pure/Thy/sessions.scala

--- a/src/Pure/Thy/sessions.scala	Mon Sep 02 10:41:14 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Sep 02 11:46:27 2019 +0200
@@ -123,7 +123,7 @@
     {
       val entries =
         for ((_, entry) <- theories.toList)
-        yield ((entry.name, ()), entry.header.imports.map(imp => theories(imp._1.theory).name))
+        yield ((entry.name, ()), entry.header.imports.map(imp => theories(imp.theory).name))
       Graph.make(entries, symmetric = true)(Document.Node.Name.Theory_Ordering)
     }
 
@@ -361,9 +361,7 @@
               (graph0 /: dependencies.entries)(
                 { case (g, entry) =>
                     val a = node(entry.name)
-                    val bs =
-                      entry.header.imports.map({ case (name, _) => node(name) }).
-                        filterNot(_ == a)
+                    val bs = entry.header.imports.map(node).filterNot(_ == a)
                     ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
             }
 
@@ -375,7 +373,7 @@
 
             val used_theories =
               for ((options, name) <- dependencies.adjunct_theories)
-              yield ((name, options), known.theories(name.theory).imports)
+              yield ((name, options), known.theories(name.theory).header.imports)
 
             val sources_errors =
               for (p <- session_files if !p.is_file) yield "No such file: " + p