--- a/src/Pure/Isar/isar_cmd.ML Wed Aug 13 22:29:43 2014 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Thu Aug 14 10:48:40 2014 +0200
@@ -39,9 +39,6 @@
val thy_deps: Toplevel.transition -> Toplevel.transition
val locale_deps: Toplevel.transition -> Toplevel.transition
val class_deps: Toplevel.transition -> Toplevel.transition
- val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
- val unused_thms: (string list * string list option) option ->
- Toplevel.transition -> Toplevel.transition
val print_stmts: string list * (Facts.ref * Attrib.src list) list
-> Toplevel.transition -> Toplevel.transition
val print_thms: string list * (Facts.ref * Attrib.src list) list
@@ -314,28 +311,6 @@
|> sort (int_ord o pairself #1) |> map #2;
in Graph_Display.display_graph gr end);
-fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
- Thm_Deps.thm_deps (Toplevel.theory_of state)
- (Attrib.eval_thms (Toplevel.context_of state) args));
-
-
-(* find unused theorems *)
-
-fun unused_thms opt_range = Toplevel.keep (fn state =>
- let
- val thy = Toplevel.theory_of state;
- val ctxt = Toplevel.context_of state;
- fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
- val get_theory = Context.get_theory thy;
- in
- Thm_Deps.unused_thms
- (case opt_range of
- NONE => (Theory.parents_of thy, [thy])
- | SOME (xs, NONE) => (map get_theory xs, [thy])
- | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
- |> map pretty_thm |> Pretty.writeln_chunks
- end);
-
(* print theorems, terms, types etc. *)