structure Thm_Deps;
authorwenzelm
Mon Nov 02 21:05:47 2009 +0100 (2009-11-02)
changeset 3339191b9da2a7b44
parent 33390 5b499f36dd25
child 33392 73c8987dc9f0
structure Thm_Deps;
src/Pure/Isar/isar_cmd.ML
src/Pure/Thy/thm_deps.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Nov 02 21:03:41 2009 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Nov 02 21:05:47 2009 +0100
     1.3 @@ -408,7 +408,7 @@
     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 -  ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
     1.8 +  Thm_Deps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
     1.9  
    1.10  
    1.11  (* find unused theorems *)
    1.12 @@ -419,7 +419,7 @@
    1.13      val ctxt = Toplevel.context_of state;
    1.14      fun pretty_thm (a, th) = ProofContext.pretty_fact ctxt (a, [th]);
    1.15    in
    1.16 -    ThmDeps.unused_thms
    1.17 +    Thm_Deps.unused_thms
    1.18        (case opt_range of
    1.19          NONE => (Theory.parents_of thy, [thy])
    1.20        | SOME (xs, NONE) => (map ThyInfo.get_theory xs, [thy])
     2.1 --- a/src/Pure/Thy/thm_deps.ML	Mon Nov 02 21:03:41 2009 +0100
     2.2 +++ b/src/Pure/Thy/thm_deps.ML	Mon Nov 02 21:05:47 2009 +0100
     2.3 @@ -10,7 +10,7 @@
     2.4    val unused_thms: theory list * theory list -> (string * thm) list
     2.5  end;
     2.6  
     2.7 -structure ThmDeps: THM_DEPS =
     2.8 +structure Thm_Deps: THM_DEPS =
     2.9  struct
    2.10  
    2.11  (* thm_deps *)