src/Pure/Thy/thm_deps.ML
changeset 37870 dd9cfc512b7f
parent 37216 3165bc303f66
child 39557 fe5722fce758
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Wed Jul 21 15:13:36 2010 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Wed Jul 21 15:23:46 2010 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature THM_DEPS =
     1.6  sig
     1.7 -  val thm_deps: thm list -> unit
     1.8 +  val thm_deps: theory -> thm list -> unit
     1.9    val unused_thms: theory list * theory list -> (string * thm) list
    1.10  end;
    1.11  
    1.12 @@ -15,7 +15,7 @@
    1.13  
    1.14  (* thm_deps *)
    1.15  
    1.16 -fun thm_deps thms =
    1.17 +fun thm_deps thy thms =
    1.18    let
    1.19      fun add_dep ("", _, _) = I
    1.20        | add_dep (name, _, PBody {thms = thms', ...}) =
    1.21 @@ -24,7 +24,7 @@
    1.22              val session =
    1.23                (case prefix of
    1.24                  a :: _ =>
    1.25 -                  (case Thy_Info.lookup_theory a of
    1.26 +                  (case try (Context.get_theory thy) a of
    1.27                      SOME thy =>
    1.28                        (case Present.session_name thy of
    1.29                          "" => []