src/Pure/Thy/thm_deps.ML
changeset 16894 40f80823b451
parent 16268 d978482479d3
child 17020 f3014afac46f
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Tue Jul 19 20:47:00 2005 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Tue Jul 19 20:47:01 2005 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4        let val ((name, tags), prf') = dest_thm_axm prf
     1.5        in
     1.6          if name <> "" andalso not (Drule.has_internal tags) then
     1.7 -          if is_none (Symtab.lookup (gra, name)) then
     1.8 +          if not (Symtab.defined gra name) then
     1.9              let
    1.10                val (gra', parents') = make_deps_graph ((gra, []), prf');
    1.11                val prefx = #1 (Library.split_last (NameSpace.unpack name));