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