# HG changeset patch
# User wenzelm
# Date 1491334646 -7200
# Node ID 6e47a27e3d4380f3d7eaa4ee5145e67a9011c03a
# Parent  4ad983094226b7152a21550c2cd7f420afce333c
tuned signature;

diff -r 4ad983094226 -r 6e47a27e3d43 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Tue Apr 04 21:33:51 2017 +0200
+++ b/src/Pure/Thy/present.scala	Tue Apr 04 21:37:26 2017 +0200
@@ -18,19 +18,19 @@
 
   def session_graph(
     parent_session: String,
-    parent_loaded: String => Boolean,
+    parent_loaded: Document.Node.Name => Boolean,
     deps: List[Thy_Info.Dep]): Graph_Display.Graph =
   {
     val parent_session_node =
       Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
 
     def node(name: Document.Node.Name): Graph_Display.Node =
-      if (parent_loaded(name.theory)) parent_session_node
+      if (parent_loaded(name)) parent_session_node
       else Graph_Display.Node(Long_Name.base_name(name.theory), "theory." + name.theory)
 
     (Graph_Display.empty_graph /: deps) {
       case (g, dep) =>
-        if (parent_loaded(dep.name.theory)) g
+        if (parent_loaded(dep.name)) g
         else {
           val a = node(dep.name)
           val bs = dep.header.imports.map({ case (name, _) => node(name) })
diff -r 4ad983094226 -r 6e47a27e3d43 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Apr 04 21:33:51 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Apr 04 21:37:26 2017 +0200
@@ -143,7 +143,7 @@
                 sources = all_files.map(p => (p, SHA1.digest(p.file))),
                 session_graph =
                   Present.session_graph(info.parent getOrElse "",
-                    parent_base.loaded_theories, thy_deps.deps))
+                    parent_base.loaded_theory _, thy_deps.deps))
 
             deps + (name -> base)
           }