# HG changeset patch
# User aspinall
# Date 1121246948 -7200
# Node ID e8f7a6ec92e5dc6772e98014c8ee66744a3145dc
# Parent  0c6f5fe3067605de31aab4ff8bde3772b6fdf414
Note about theorem dependencies including themselves.

diff -r 0c6f5fe30676 -r e8f7a6ec92e5 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Wed Jul 13 11:28:09 2005 +0200
+++ b/src/Pure/proof_general.ML	Wed Jul 13 11:29:08 2005 +0200
@@ -470,6 +470,7 @@
 
 val spaces_quote = space_implode " " o map quote;
 
+(* FIXME: investigate why dependencies at the moment include themselves! *)
 fun thm_deps_message (thms, deps) =
   if pgip() then
     issue_pgips