# HG changeset patch
# User wenzelm
# Date 1257192347 -3600
# Node ID 91b9da2a7b440830c88e4377ded96121e5495d75
# Parent  5b499f36dd259e1ca8a6aa74dc51dee8b130f45b
structure Thm_Deps;

diff -r 5b499f36dd25 -r 91b9da2a7b44 src/Pure/Isar/isar_cmd.ML
--- 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])
diff -r 5b499f36dd25 -r 91b9da2a7b44 src/Pure/Thy/thm_deps.ML
--- 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 *)