--- a/src/Pure/Thy/thm_deps.ML Sun May 17 07:17:39 2009 +0200
+++ b/src/Pure/Thy/thm_deps.ML Mon May 18 09:48:06 2009 +0200
@@ -66,7 +66,7 @@
case Thm.get_group thm of
NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty;
val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') =>
- if member (op =) [Thm.theoremK, Thm.generated_theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
+ if member (op =) [Thm.theoremK, Thm.generatedK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
andalso is_unused p
then
(case Thm.get_group thm of