src/Pure/Isar/isar_cmd.ML

--- a/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:13:11 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:15:52 2014 +0100
@@ -275,25 +275,26 @@
     val thy = Toplevel.theory_of state;
     val thy_session = Present.session_name thy;
 
-    val graph = rev (Theory.nodes_of thy) |> map (fn node =>
+    val gr_nodes = rev (Theory.nodes_of thy) |> map (fn node =>
       let
         val name = Context.theory_name node;
         val parents = map Context.theory_name (Theory.parents_of node);
         val session = Present.session_name node;
         val unfold = (session = thy_session);
       in
-       {name = name, ident = name, parents = parents, directory = session,
-        unfold = unfold, path = "", content = []}
+       ((name, Graph_Display.session_node
+         {name = name, directory = session, unfold = unfold, path = ""}), parents)
       end);
-  in Graph_Display.display_graph graph end);
+  in Graph_Display.display_graph (map (fst o fst) gr_nodes, Graph.make gr_nodes) end);
 
 val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   let
     val thy = Toplevel.theory_of state;
-    val graph = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} =>
-     {name = Locale.extern thy name, ident = name, parents = parents,
-      directory = "", unfold = true, path = "", content = [body]});
-  in Graph_Display.display_graph graph end);
+    val gr = Locale.pretty_locale_deps thy
+      |> map (fn {name, parents, body} => ((name,
+          Graph_Display.content_node (Locale.extern thy name) [body]), parents))
+      |> Graph.make;
+  in Graph_Display.display_graph ([], gr) end);
 
 
 (* print theorems, terms, types etc. *)