# HG changeset patch
# User wenzelm
# Date 1303826175 -7200
# Node ID aca720fb393661d79c6594858fc0ea46aac96cfc
# Parent  8a33a5596ba89ffaa578e595926c6942bcab9891
mark thm tag "kind" as legacy;

diff -r 8a33a5596ba8 -r aca720fb3936 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Tue Apr 26 09:50:17 2011 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Tue Apr 26 15:56:15 2011 +0200
@@ -80,7 +80,8 @@
 
     val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
       if not concealed andalso
-        member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.get_kind th) andalso
+        (* FIXME replace by robust treatment of thm groups *)
+        member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) andalso
         is_unused a
       then
         (case group of
diff -r 8a33a5596ba8 -r aca720fb3936 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Apr 26 09:50:17 2011 +0200
+++ b/src/Pure/more_thm.ML	Tue Apr 26 15:56:15 2011 +0200
@@ -90,7 +90,7 @@
   val theoremK: string
   val lemmaK: string
   val corollaryK: string
-  val get_kind: thm -> string
+  val legacy_get_kind: thm -> string
   val kind_rule: string -> thm -> thm
   val kind: string -> attribute
 end;
@@ -453,7 +453,7 @@
 val lemmaK = "lemma";
 val corollaryK = "corollary";
 
-fun get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);
+fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);
 
 fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN;
 fun kind k x = if k = "" then x else rule_attribute (K (kind_rule k)) x;