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