--- 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
--- 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;