diff -r 6c2373adc7a0 -r 30ab97554602 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Jan 31 20:06:24 2007 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Jan 31 20:07:40 2007 +0100
@@ -212,14 +212,13 @@
 fun thm_deps_message (thms, deps) =
   emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
 
-(* FIXME: check this uses non-transitive closure function here *)
 fun tell_thm_deps ths =
   if Output.has_mode thm_depsN then
     let
-      val names = filter_out (equal "") (map PureThy.get_name_hint ths); (* da: HAS THIS NOW BECOME "??.unknown"? *)
-      val deps = filter_out (equal "")
-        (Symtab.keys (fold Proofterm.thms_of_proof
-          (map Thm.proof_of ths) Symtab.empty));
+      val names = filter_out (equal PureThy.unknown_name_hint) 
+			     (map PureThy.get_name_hint ths); 
+      val deps = Symtab.keys (fold Proofterm.thms_of_proof'
+				   (map Thm.proof_of ths) Symtab.empty);
     in
       if null names orelse null deps then ()
       else thm_deps_message (spaces_quote names, spaces_quote deps)