--- a/src/Tools/Code/code_thingol.ML Wed Dec 31 14:08:50 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML Wed Dec 31 14:13:11 2014 +0100
@@ -927,7 +927,7 @@
fun namify consts = map (Code.string_of_const thy) consts
|> commas;
val graph = map (fn (consts, constss) =>
- { name = namify consts, ID = namify consts, dir = "", unfold = true,
+ { name = namify consts, ident = namify consts, directory = "", unfold = true,
path = "", parents = map namify constss, content = [] }) conn;
in Graph_Display.display_graph graph end;