# HG changeset patch
# User wenzelm
# Date 1258059575 -3600
# Node ID d983509dbf31004fa8e5a6681501e8532a19d2f6
# Parent  af07d9cd86cef5a947a90536bab01ddacb4b8d8c
unused_thms: ignore kind -- already observes "concealed" flag;

diff -r af07d9cd86ce -r d983509dbf31 src/Pure/Thy/thm_deps.ML
--- 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 =>