--- a/src/Pure/Thy/thm_deps.ML Thu Nov 12 20:33:26 2009 +0100
+++ b/src/Pure/Thy/thm_deps.ML Thu Nov 12 21:59:35 2009 +0100
@@ -79,9 +79,7 @@
NONE => I
| SOME grp => Inttab.update (grp, ()))) thms Inttab.empty;
val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, grps') =>
- if member (op =) [Thm.theoremK, Thm.generatedK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK]
- (Thm.get_kind th) andalso not concealed andalso is_unused (a, th)
- then
+ if not concealed andalso is_unused (a, th) then
(case group of
NONE => ((a, th) :: thms, grps')
| SOME grp =>