diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/ProofGeneral/proof_general_pgip.ML
--- 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