thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
authorwenzelm
Wed Jul 21 15:23:46 2010 +0200 (2010-07-21)
changeset 37870dd9cfc512b7f
parent 37869 e9c6a7fe1989
child 37871 c7ce7685e087
thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
src/Pure/Isar/isar_cmd.ML
src/Pure/Thy/thm_deps.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Jul 21 15:13:36 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Jul 21 15:23:46 2010 +0200
     1.3 @@ -434,7 +434,8 @@
     1.4    in Present.display_graph gr end);
     1.5  
     1.6  fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
     1.7 -  Thm_Deps.thm_deps (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
     1.8 +  Thm_Deps.thm_deps (Toplevel.theory_of state)
     1.9 +    (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
    1.10  
    1.11  
    1.12  (* find unused theorems *)
    1.13 @@ -444,12 +445,13 @@
    1.14      val thy = Toplevel.theory_of state;
    1.15      val ctxt = Toplevel.context_of state;
    1.16      fun pretty_thm (a, th) = ProofContext.pretty_fact ctxt (a, [th]);
    1.17 +    val get_theory = Context.get_theory thy;
    1.18    in
    1.19      Thm_Deps.unused_thms
    1.20        (case opt_range of
    1.21          NONE => (Theory.parents_of thy, [thy])
    1.22 -      | SOME (xs, NONE) => (map Thy_Info.get_theory xs, [thy])
    1.23 -      | SOME (xs, SOME ys) => (map Thy_Info.get_theory xs, map Thy_Info.get_theory ys))
    1.24 +      | SOME (xs, NONE) => (map get_theory xs, [thy])
    1.25 +      | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
    1.26      |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
    1.27    end);
    1.28  
     2.1 --- a/src/Pure/Thy/thm_deps.ML	Wed Jul 21 15:13:36 2010 +0200
     2.2 +++ b/src/Pure/Thy/thm_deps.ML	Wed Jul 21 15:23:46 2010 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  
     2.5  signature THM_DEPS =
     2.6  sig
     2.7 -  val thm_deps: thm list -> unit
     2.8 +  val thm_deps: theory -> thm list -> unit
     2.9    val unused_thms: theory list * theory list -> (string * thm) list
    2.10  end;
    2.11  
    2.12 @@ -15,7 +15,7 @@
    2.13  
    2.14  (* thm_deps *)
    2.15  
    2.16 -fun thm_deps thms =
    2.17 +fun thm_deps thy thms =
    2.18    let
    2.19      fun add_dep ("", _, _) = I
    2.20        | add_dep (name, _, PBody {thms = thms', ...}) =
    2.21 @@ -24,7 +24,7 @@
    2.22              val session =
    2.23                (case prefix of
    2.24                  a :: _ =>
    2.25 -                  (case Thy_Info.lookup_theory a of
    2.26 +                  (case try (Context.get_theory thy) a of
    2.27                      SOME thy =>
    2.28                        (case Present.session_name thy of
    2.29                          "" => []