# HG changeset patch
# User wenzelm
# Date 1030541263 -7200
# Node ID fcdbd6cf5f9f444b07f83fb343a34a73cf3f8e81
# Parent  895994073bdf007a1abd735baa782e3bcb9bc826
improved tell_thm_deps;

diff -r 895994073bdf -r fcdbd6cf5f9f src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Wed Aug 28 13:08:50 2002 +0200
+++ b/src/Pure/proof_general.ML	Wed Aug 28 15:27:43 2002 +0200
@@ -165,18 +165,18 @@
 
 local
 
+val spaces_quote = space_implode " " o map quote;
+
 fun tell_thm_deps ths =
   conditional (thm_depsN mem_string ! print_mode) (fn () =>
     let
-      val names = map Thm.name_of_thm ths;
-      val refs =
-        foldl (uncurry Proofterm.thms_of_proof) (Symtab.empty, map Thm.proof_of ths)
-        |> Symtab.keys;
-      val deps = refs \\ names \ "";
+      val names = map Thm.name_of_thm ths \ "";
+      val deps = Symtab.keys (foldl (uncurry Proofterm.thms_of_proof)
+          (Symtab.empty, map Thm.proof_of ths)) \ "";
     in
-      if null deps then ()
-      else notify ("Proof General, theorem dependencies are: "
-        ^ space_implode " " (map quote deps))    (* FIXME output names \ "" as well!? *)
+      if null names orelse null deps then ()
+      else notify ("Proof General, theorem dependencies of " ^ spaces_quote names ^ " are "
+        ^ spaces_quote deps)
     end);
 
 in