src/Pure/Tools/find_theorems.ML
changeset 39557 fe5722fce758
parent 38335 630f379f2660
child 41835 9712fae15200
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Sep 20 15:29:53 2010 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Sep 20 16:05:25 2010 +0200
     1.3 @@ -350,7 +350,7 @@
     1.4  fun nicer_shortest ctxt =
     1.5    let
     1.6      (* FIXME global name space!? *)
     1.7 -    val space = Facts.space_of (PureThy.facts_of (ProofContext.theory_of ctxt));
     1.8 +    val space = Facts.space_of (Global_Theory.facts_of (ProofContext.theory_of ctxt));
     1.9  
    1.10      val shorten =
    1.11        Name_Space.extern_flags
    1.12 @@ -381,7 +381,7 @@
    1.13        |> filter_out (Facts.is_concealed facts o #1);
    1.14    in
    1.15      maps Facts.selections
    1.16 -     (visible_facts (PureThy.facts_of (ProofContext.theory_of ctxt)) @
    1.17 +     (visible_facts (Global_Theory.facts_of (ProofContext.theory_of ctxt)) @
    1.18        visible_facts (ProofContext.facts_of ctxt))
    1.19    end;
    1.20