src/Pure/Thy/thm_deps.ML
changeset 31174 f1f1e9b53c81
parent 30364 577edc39b501
child 31177 c39994cb152a
--- a/src/Pure/Thy/thm_deps.ML	Sat May 16 15:24:35 2009 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Sat May 16 20:17:59 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.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
+      if member (op =) [Thm.theoremK, Thm.generated_theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
         andalso is_unused p
       then
         (case Thm.get_group thm of