src/Pure/Thy/thm_deps.ML
changeset 31174 f1f1e9b53c81
parent 30364 577edc39b501
child 31177 c39994cb152a
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Sat May 16 15:24:35 2009 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Sat May 16 20:17:59 2009 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4        case Thm.get_group thm of
     1.5          NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty;
     1.6      val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') =>
     1.7 -      if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
     1.8 +      if member (op =) [Thm.theoremK, Thm.generated_theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
     1.9          andalso is_unused p
    1.10        then
    1.11          (case Thm.get_group thm of