src/Pure/Isar/isar_cmd.ML
changeset 58201 5bf56c758e02
parent 58011 bc6bced136e5
child 58868 c5e1cce7ace3
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Sep 07 14:39:23 2014 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Sep 07 17:51:28 2014 +0200
     1.3 @@ -38,7 +38,6 @@
     1.4    val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
     1.5    val thy_deps: Toplevel.transition -> Toplevel.transition
     1.6    val locale_deps: Toplevel.transition -> Toplevel.transition
     1.7 -  val class_deps: Toplevel.transition -> Toplevel.transition
     1.8    val print_stmts: string list * (Facts.ref * Token.src list) list
     1.9      -> Toplevel.transition -> Toplevel.transition
    1.10    val print_thms: string list * (Facts.ref * Token.src list) list
    1.11 @@ -298,19 +297,6 @@
    1.12        dir = "", unfold = true, path = "", content = [body]});
    1.13    in Graph_Display.display_graph gr end);
    1.14  
    1.15 -val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.16 -  let
    1.17 -    val ctxt = Toplevel.context_of state;
    1.18 -    val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
    1.19 -    val classes = Sorts.classes_of algebra;
    1.20 -    fun entry (c, (i, (_, cs))) =
    1.21 -      (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
    1.22 -            dir = "", unfold = true, path = "", content = []});
    1.23 -    val gr =
    1.24 -      Graph.fold (cons o entry) classes []
    1.25 -      |> sort (int_ord o pairself #1) |> map #2;
    1.26 -  in Graph_Display.display_graph gr end);
    1.27 -
    1.28  
    1.29  (* print theorems, terms, types etc. *)
    1.30