src/Pure/Thy/thm_deps.ML
changeset 33642 d983509dbf31
parent 33391 91b9da2a7b44
child 33769 6d8630fab26a
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Thu Nov 12 20:33:26 2009 +0100
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Thu Nov 12 21:59:35 2009 +0100
     1.3 @@ -79,9 +79,7 @@
     1.4            NONE => I
     1.5          | SOME grp => Inttab.update (grp, ()))) thms Inttab.empty;
     1.6      val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, grps') =>
     1.7 -      if member (op =) [Thm.theoremK, Thm.generatedK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK]
     1.8 -        (Thm.get_kind th) andalso not concealed andalso is_unused (a, th)
     1.9 -      then
    1.10 +      if not concealed andalso is_unused (a, th) then
    1.11          (case group of
    1.12             NONE => ((a, th) :: thms, grps')
    1.13           | SOME grp =>