src/Pure/Thy/thm_deps.ML
changeset 39557 fe5722fce758
parent 37870 dd9cfc512b7f
child 41489 8e2b8649507d
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Mon Sep 20 15:29:53 2010 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Mon Sep 20 16:05:25 2010 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4  fun unused_thms (base_thys, thys) =
     1.5    let
     1.6      fun add_fact space (name, ths) =
     1.7 -      if exists (fn thy => PureThy.defined_fact thy name) base_thys then I
     1.8 +      if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
     1.9        else
    1.10          let val {concealed, group, ...} = Name_Space.the_entry space name in
    1.11            fold_rev (fn th =>
    1.12 @@ -60,7 +60,7 @@
    1.13      fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
    1.14  
    1.15      val new_thms =
    1.16 -      fold (add_facts o PureThy.facts_of) thys []
    1.17 +      fold (add_facts o Global_Theory.facts_of) thys []
    1.18        |> sort_distinct (string_ord o pairself #1);
    1.19  
    1.20      val used =