src/Pure/Isar/isar_cmd.ML
changeset 57934 5e500c0e7eca
parent 57683 cc0aa6528890
child 58011 bc6bced136e5
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Aug 13 22:29:43 2014 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Aug 14 10:48:40 2014 +0200
     1.3 @@ -39,9 +39,6 @@
     1.4    val thy_deps: Toplevel.transition -> Toplevel.transition
     1.5    val locale_deps: Toplevel.transition -> Toplevel.transition
     1.6    val class_deps: Toplevel.transition -> Toplevel.transition
     1.7 -  val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
     1.8 -  val unused_thms: (string list * string list option) option ->
     1.9 -    Toplevel.transition -> Toplevel.transition
    1.10    val print_stmts: string list * (Facts.ref * Attrib.src list) list
    1.11      -> Toplevel.transition -> Toplevel.transition
    1.12    val print_thms: string list * (Facts.ref * Attrib.src list) list
    1.13 @@ -314,28 +311,6 @@
    1.14        |> sort (int_ord o pairself #1) |> map #2;
    1.15    in Graph_Display.display_graph gr end);
    1.16  
    1.17 -fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.18 -  Thm_Deps.thm_deps (Toplevel.theory_of state)
    1.19 -    (Attrib.eval_thms (Toplevel.context_of state) args));
    1.20 -
    1.21 -
    1.22 -(* find unused theorems *)
    1.23 -
    1.24 -fun unused_thms opt_range = Toplevel.keep (fn state =>
    1.25 -  let
    1.26 -    val thy = Toplevel.theory_of state;
    1.27 -    val ctxt = Toplevel.context_of state;
    1.28 -    fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
    1.29 -    val get_theory = Context.get_theory thy;
    1.30 -  in
    1.31 -    Thm_Deps.unused_thms
    1.32 -      (case opt_range of
    1.33 -        NONE => (Theory.parents_of thy, [thy])
    1.34 -      | SOME (xs, NONE) => (map get_theory xs, [thy])
    1.35 -      | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
    1.36 -    |> map pretty_thm |> Pretty.writeln_chunks
    1.37 -  end);
    1.38 -
    1.39  
    1.40  (* print theorems, terms, types etc. *)
    1.41