src/Pure/proof_general.ML

   else emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
 
 (* FIXME: check this uses non-transitive closure function here *)
 fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
   let
-    val names = filter_out (equal "") (map Thm.name_of_thm ths);
+    val names = filter_out (equal "") (map PureThy.get_name_hint ths);
     val deps = filter_out (equal "")
       (Symtab.keys (fold Proofterm.thms_of_proof
         (map Thm.proof_of ths) Symtab.empty));
   in
     if null names orelse null deps then ()