--- a/src/Pure/Isar/isar_cmd.ML Sun Sep 07 14:39:23 2014 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sun Sep 07 17:51:28 2014 +0200
@@ -38,7 +38,6 @@
val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
val thy_deps: Toplevel.transition -> Toplevel.transition
val locale_deps: Toplevel.transition -> Toplevel.transition
- val class_deps: Toplevel.transition -> Toplevel.transition
val print_stmts: string list * (Facts.ref * Token.src list) list
-> Toplevel.transition -> Toplevel.transition
val print_thms: string list * (Facts.ref * Token.src list) list
@@ -298,19 +297,6 @@
dir = "", unfold = true, path = "", content = [body]});
in Graph_Display.display_graph gr end);
-val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
- let
- val ctxt = Toplevel.context_of state;
- val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
- val classes = Sorts.classes_of algebra;
- fun entry (c, (i, (_, cs))) =
- (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
- dir = "", unfold = true, path = "", content = []});
- val gr =
- Graph.fold (cons o entry) classes []
- |> sort (int_ord o pairself #1) |> map #2;
- in Graph_Display.display_graph gr end);
-
(* print theorems, terms, types etc. *)