src/Pure/Isar/isar_cmd.ML
changeset 60100 3c66b0a9d7b0
parent 60099 d20ca79d50e4
child 60378 26dcc7f19b02
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 15:22:44 2015 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 16:19:39 2015 +0200
     1.3 @@ -35,7 +35,6 @@
     1.4    val diag_state: Proof.context -> Toplevel.state
     1.5    val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
     1.6    val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
     1.7 -  val locale_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 @@ -264,16 +263,6 @@
    1.12      in Proof_Display.pretty_theorems_diff verbose prev_thys thy end;
    1.13  
    1.14  
    1.15 -(* display dependencies *)
    1.16 -
    1.17 -val locale_deps =
    1.18 -  Toplevel.keep (Toplevel.theory_of #> (fn thy =>
    1.19 -    Locale.pretty_locale_deps thy
    1.20 -    |> map (fn {name, parents, body} =>
    1.21 -      ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
    1.22 -    |> Graph_Display.display_graph));
    1.23 -
    1.24 -
    1.25  (* print theorems, terms, types etc. *)
    1.26  
    1.27  local