src/Pure/Thy/thm_deps.ML
changeset 18799 f137c5e971f5
parent 17412 e26cb20ef0cc
child 20578 f26c8408a675
--- a/src/Pure/Thy/thm_deps.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/Pure/Thy/thm_deps.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -39,7 +39,7 @@
   | make_deps_graph prf = (fn p as (gra, parents) =>
       let val ((name, tags), prf') = dest_thm_axm prf
       in
-        if name <> "" andalso not (Drule.has_internal tags) then
+        if name <> "" andalso not (PureThy.has_internal tags) then
           if not (Symtab.defined gra name) then
             let
               val (gra', parents') = make_deps_graph prf' (gra, []);