src/Pure/Isar/isar_cmd.ML
changeset 60095 c48d536231fe
parent 60082 d3573eb7728f
child 60096 96a4765ba7d1
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 13:39:21 2015 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 13:48:10 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 thy_deps: Toplevel.transition -> Toplevel.transition
     1.8    val locale_deps: Toplevel.transition -> Toplevel.transition
     1.9    val print_stmts: string list * (Facts.ref * Token.src list) list
    1.10      -> Toplevel.transition -> Toplevel.transition
    1.11 @@ -270,15 +269,6 @@
    1.12  
    1.13  (* display dependencies *)
    1.14  
    1.15 -val thy_deps =
    1.16 -  Toplevel.unknown_theory o
    1.17 -  Toplevel.keep (fn st =>
    1.18 -    let
    1.19 -      val thy = Toplevel.theory_of st;
    1.20 -      val parent_session = Session.get_name ();
    1.21 -      val parent_loaded = is_some o Thy_Info.lookup_theory;
    1.22 -    in Graph_Display.display_graph (Present.session_graph parent_session parent_loaded thy) end);
    1.23 -
    1.24  val locale_deps =
    1.25    Toplevel.unknown_theory o
    1.26    Toplevel.keep (Toplevel.theory_of #> (fn thy =>