--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Apr 16 13:48:45 2011 +0200
@@ -517,12 +517,15 @@
local
-fun theory_facts name =
+fun theory_facts thy =
+ (map Global_Theory.facts_of (Theory.parents_of thy), Global_Theory.facts_of thy);
+
+fun thms_of_thy name =
let val thy = Thy_Info.get_theory name
- in (map Global_Theory.facts_of (Theory.parents_of thy), Global_Theory.facts_of thy) end;
+ in map fst (theory_facts thy |-> Facts.extern_static (ProofContext.init_global thy)) end;
-fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static);
-fun qualified_thms_of_thy name = map fst (theory_facts name |-> Facts.dest_static);
+fun qualified_thms_of_thy name =
+ map fst (theory_facts (Thy_Info.get_theory name) |-> Facts.dest_static);
in