--- a/src/Pure/Isar/isar_cmd.ML Mon Nov 02 21:03:41 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Mon Nov 02 21:05:47 2009 +0100
@@ -408,7 +408,7 @@
in Present.display_graph gr end);
fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
- ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
+ Thm_Deps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
(* find unused theorems *)
@@ -419,7 +419,7 @@
val ctxt = Toplevel.context_of state;
fun pretty_thm (a, th) = ProofContext.pretty_fact ctxt (a, [th]);
in
- ThmDeps.unused_thms
+ Thm_Deps.unused_thms
(case opt_range of
NONE => (Theory.parents_of thy, [thy])
| SOME (xs, NONE) => (map ThyInfo.get_theory xs, [thy])
--- a/src/Pure/Thy/thm_deps.ML Mon Nov 02 21:03:41 2009 +0100
+++ b/src/Pure/Thy/thm_deps.ML Mon Nov 02 21:05:47 2009 +0100
@@ -10,7 +10,7 @@
val unused_thms: theory list * theory list -> (string * thm) list
end;
-structure ThmDeps: THM_DEPS =
+structure Thm_Deps: THM_DEPS =
struct
(* thm_deps *)