# HG changeset patch
# User haftmann
# Date 1421926784 -3600
# Node ID 3a0044e95ebac07a4b6de4629fbd755a12a2588a
# Parent  db6ecef63d5ba54e06a24b40cfe8200d56a601b2
backed out obsolete workaround from ef1edfb36af7

diff -r db6ecef63d5b -r 3a0044e95eba src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Jan 21 18:40:03 2015 +0100
+++ b/src/Pure/Isar/class.ML	Thu Jan 22 12:39:44 2015 +0100
@@ -51,7 +51,7 @@
   val default_intro_tac: Proof.context -> thm list -> tactic
 
   (*diagnostics*)
-  val pretty_specification: theory -> class -> Pretty.T list * Pretty.T list
+  val pretty_specification: theory -> class -> Pretty.T list
 end;
 
 structure Class: CLASS =
@@ -750,8 +750,8 @@
         else
           maps (Element.pretty_ctxt_no_attribs class_ctxt) (fixes @ assumes)
           |> maps (fn prt => [Pretty.fbrk, prt]);
-    in (header, body) end
-  else ([], []);
+    in if null body then [] else [Pretty.block (header @ body)] end
+  else [];
 
 end;
 
diff -r db6ecef63d5b -r 3a0044e95eba src/Pure/Tools/class_deps.ML
--- a/src/Pure/Tools/class_deps.ML	Wed Jan 21 18:40:03 2015 +0100
+++ b/src/Pure/Tools/class_deps.ML	Thu Jan 22 12:39:44 2015 +0100
@@ -6,7 +6,6 @@
 
 signature CLASS_DEPS =
 sig
-  val inlined_class_specs: bool Config.T
   val class_deps: Proof.context -> sort list option -> sort list option -> unit
   val class_deps_cmd: Proof.context -> string list option -> string list option -> unit
 end;
@@ -14,10 +13,6 @@
 structure Class_Deps: CLASS_DEPS =
 struct
 
-val inlined_class_specs = Attrib.setup_config_bool @{binding "inlined_class_specs"} (K false);
-
-val stringify = XML.content_of o YXML.parse_body o Pretty.string_of;
-
 fun gen_class_deps prep_sort ctxt raw_subs raw_supers =
   let
     val thy = Proof_Context.theory_of ctxt;
@@ -34,23 +29,9 @@
     val (_, algebra) =
       Sorts.subalgebra (Context.pretty ctxt)
         (le_sub andf super_le) (K NONE) original_algebra;
-    val inlined = Config.get ctxt inlined_class_specs;
-    fun label_for c =
-      if inlined
-      then (stringify o Pretty.block o op @) (Class.pretty_specification thy c)
-      else Name_Space.extern ctxt space c;
-    fun tooltip_for c =
-      if inlined
-      then []
-      else
-        let
-          val pretty_spec = Class.pretty_specification thy c
-        in
-          if (null o snd) pretty_spec
-          then []
-          else [(Pretty.block o op @) pretty_spec]
-        end;
-    fun node c = Graph_Display.content_node (label_for c) (tooltip_for c);
+    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