diff -r 4642cf4a7ebb -r f529719cc47d src/Pure/General/graph_display.scala
--- a/src/Pure/General/graph_display.scala	Mon Oct 09 21:12:22 2017 +0200
+++ b/src/Pure/General/graph_display.scala	Mon Oct 09 21:43:27 2017 +0200
@@ -60,5 +60,13 @@
         import XML.Decode._
         list(pair(pair(string, pair(string, x => x)), list(string)))(body)
       })
+
+  def make_graph[A](
+    graph: isabelle.Graph[String, A],
+    name: (String, A) => String = (x: String, a: A) => x): Graph =
+  {
+    val entries =
+      (for ((x, (a, (ps, _))) <- graph.iterator) yield ((x, (name(x, a), Nil)), ps.toList)).toList
+    build_graph(entries)
+  }
 }
-