Note about theorem dependencies including themselves.
authoraspinall
Wed Jul 13 11:29:08 2005 +0200 (2005-07-13)
changeset 16789e8f7a6ec92e5
parent 16788 0c6f5fe30676
child 16790 be2780f435e1
Note about theorem dependencies including themselves.
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Wed Jul 13 11:28:09 2005 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Wed Jul 13 11:29:08 2005 +0200
     1.3 @@ -470,6 +470,7 @@
     1.4  
     1.5  val spaces_quote = space_implode " " o map quote;
     1.6  
     1.7 +(* FIXME: investigate why dependencies at the moment include themselves! *)
     1.8  fun thm_deps_message (thms, deps) =
     1.9    if pgip() then
    1.10      issue_pgips