src/Pure/General/graph_display.ML

--- a/src/Pure/General/graph_display.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/General/graph_display.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -65,8 +65,9 @@
 fun build_graph entries =
   let
     val ident_names =
-      fold (fn ((ident, Node {name, ...}), _) => Symtab.update_new (ident, (name, ident)))
-        entries Symtab.empty;
+      Symtab.build
+        (entries |> fold (fn ((ident, Node {name, ...}), _) =>
+          Symtab.update_new (ident, (name, ident))));
     val the_key = the o Symtab.lookup ident_names;
   in
     Graph.empty