# HG changeset patch
# User wenzelm
# Date 1279718626 -7200
# Node ID dd9cfc512b7f9ca58d499385d48cf66e7e01ce81
# Parent  e9c6a7fe1989b03daba9ab8b761f1ba76767aa7a
thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;

diff -r e9c6a7fe1989 -r dd9cfc512b7f src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Jul 21 15:13:36 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Jul 21 15:23:46 2010 +0200
@@ -434,7 +434,8 @@
   in Present.display_graph gr end);
 
 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  Thm_Deps.thm_deps (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
+  Thm_Deps.thm_deps (Toplevel.theory_of state)
+    (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
 
 
 (* find unused theorems *)
@@ -444,12 +445,13 @@
     val thy = Toplevel.theory_of state;
     val ctxt = Toplevel.context_of state;
     fun pretty_thm (a, th) = ProofContext.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 Thy_Info.get_theory xs, [thy])
-      | SOME (xs, SOME ys) => (map Thy_Info.get_theory xs, map Thy_Info.get_theory ys))
+      | SOME (xs, NONE) => (map get_theory xs, [thy])
+      | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
     |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
   end);
 
diff -r e9c6a7fe1989 -r dd9cfc512b7f src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Wed Jul 21 15:13:36 2010 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Wed Jul 21 15:23:46 2010 +0200
@@ -6,7 +6,7 @@
 
 signature THM_DEPS =
 sig
-  val thm_deps: thm list -> unit
+  val thm_deps: theory -> thm list -> unit
   val unused_thms: theory list * theory list -> (string * thm) list
 end;
 
@@ -15,7 +15,7 @@
 
 (* thm_deps *)
 
-fun thm_deps thms =
+fun thm_deps thy thms =
   let
     fun add_dep ("", _, _) = I
       | add_dep (name, _, PBody {thms = thms', ...}) =
@@ -24,7 +24,7 @@
             val session =
               (case prefix of
                 a :: _ =>
-                  (case Thy_Info.lookup_theory a of
+                  (case try (Context.get_theory thy) a of
                     SOME thy =>
                       (case Present.session_name thy of
                         "" => []