diff -r 827730aea9e8 -r 27a8ad9612a3 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -341,7 +341,7 @@
 fun tell_thm_deps ths =
   if !show_theorem_dependencies then
       let
-        val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths);
+        val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
         val deps = (Symtab.keys (fold Proofterm.thms_of_proof'
                                         (map Thm.proof_of ths) Symtab.empty))
       in