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, []);