src/Pure/Tools/class_deps.ML
changeset 59383 1434ef1e0ede
parent 59301 9089639ba348
child 59420 ef1edfb36af7
--- a/src/Pure/Tools/class_deps.ML	Fri Jan 16 23:24:29 2015 +0100
+++ b/src/Pure/Tools/class_deps.ML	Sat Jan 17 16:40:10 2015 +0100
@@ -27,12 +27,13 @@
     val (_, algebra) =
       Sorts.subalgebra (Context.pretty ctxt)
         (le_super andf sub_le) (K NONE) original_algebra;
-    fun pretty_body_of c = if Class.is_class thy c then Class.pretty_body thy c else [];
+    fun node c =
+      Graph_Display.content_node (Name_Space.extern ctxt space c)
+        (Class.pretty_specification thy c);
   in
     Sorts.classes_of algebra
     |> Graph.dest
-    |> map (fn ((c, _), ds) =>
-        ((c, Graph_Display.content_node (Name_Space.extern ctxt space c) (pretty_body_of c)), ds))
+    |> map (fn ((c, _), ds) => ((c, node c), ds))
     |> Graph_Display.display_graph
   end;