mark thm tag "kind" as legacy;
authorwenzelm
Tue Apr 26 15:56:15 2011 +0200 (2011-04-26)
changeset 42473aca720fb3936
parent 42472 8a33a5596ba8
child 42474 8b139b8ee366
mark thm tag "kind" as legacy;
src/Pure/Thy/thm_deps.ML
src/Pure/more_thm.ML
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Tue Apr 26 09:50:17 2011 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Tue Apr 26 15:56:15 2011 +0200
     1.3 @@ -80,7 +80,8 @@
     1.4  
     1.5      val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
     1.6        if not concealed andalso
     1.7 -        member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.get_kind th) andalso
     1.8 +        (* FIXME replace by robust treatment of thm groups *)
     1.9 +        member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) andalso
    1.10          is_unused a
    1.11        then
    1.12          (case group of
     2.1 --- a/src/Pure/more_thm.ML	Tue Apr 26 09:50:17 2011 +0200
     2.2 +++ b/src/Pure/more_thm.ML	Tue Apr 26 15:56:15 2011 +0200
     2.3 @@ -90,7 +90,7 @@
     2.4    val theoremK: string
     2.5    val lemmaK: string
     2.6    val corollaryK: string
     2.7 -  val get_kind: thm -> string
     2.8 +  val legacy_get_kind: thm -> string
     2.9    val kind_rule: string -> thm -> thm
    2.10    val kind: string -> attribute
    2.11  end;
    2.12 @@ -453,7 +453,7 @@
    2.13  val lemmaK = "lemma";
    2.14  val corollaryK = "corollary";
    2.15  
    2.16 -fun get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);
    2.17 +fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);
    2.18  
    2.19  fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN;
    2.20  fun kind k x = if k = "" then x else rule_attribute (K (kind_rule k)) x;