eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
authorwenzelm
Thu Oct 29 16:34:44 2009 +0100 (2009-10-29 ago)
changeset 33315784c1b09d485
parent 33314 53d49370f7af
child 33316 6a72af4e84b8
eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
src/Pure/Isar/expression.ML
src/Pure/axclass.ML
src/Pure/more_thm.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Oct 29 16:15:33 2009 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Oct 29 16:34:44 2009 +0100
     1.3 @@ -641,8 +641,8 @@
     1.4        |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
     1.5        |> Sign.declare_const ((bname, predT), NoSyn) |> snd
     1.6        |> PureThy.add_defs false
     1.7 -        [((Binding.conceal (Binding.map_name Thm.def_name bname), Logic.mk_equals (head, body)),
     1.8 -          [Thm.kind_internal])];
     1.9 +        [((Binding.conceal (Binding.map_name Thm.def_name bname),
    1.10 +            Logic.mk_equals (head, body)), [])];
    1.11      val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
    1.12  
    1.13      val cert = Thm.cterm_of defs_thy;
     2.1 --- a/src/Pure/axclass.ML	Thu Oct 29 16:15:33 2009 +0100
     2.2 +++ b/src/Pure/axclass.ML	Thu Oct 29 16:34:44 2009 +0100
     2.3 @@ -311,7 +311,7 @@
     2.4          (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
     2.5        #>> Thm.varifyT
     2.6        #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
     2.7 -      #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [Thm.kind_internal])
     2.8 +      #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
     2.9        #> snd
    2.10        #> Sign.restore_naming thy
    2.11        #> pair (Const (c, T))))
     3.1 --- a/src/Pure/more_thm.ML	Thu Oct 29 16:15:33 2009 +0100
     3.2 +++ b/src/Pure/more_thm.ML	Thu Oct 29 16:34:44 2009 +0100
     3.3 @@ -91,13 +91,9 @@
     3.4    val lemmaK: string
     3.5    val corollaryK: string
     3.6    val internalK: string
     3.7 -  val has_kind: thm -> bool
     3.8    val get_kind: thm -> string
     3.9    val kind_rule: string -> thm -> thm
    3.10    val kind: string -> attribute
    3.11 -  val kind_internal: attribute
    3.12 -  val has_internal: Properties.property list -> bool
    3.13 -  val is_internal: thm -> bool
    3.14  end;
    3.15  
    3.16  structure Thm: THM =
    3.17 @@ -425,16 +421,10 @@
    3.18  val corollaryK = "corollary";
    3.19  val internalK = Markup.internalK;
    3.20  
    3.21 -fun the_kind thm = the (Properties.get (Thm.get_tags thm) Markup.kindN);
    3.22 -
    3.23 -val has_kind = can the_kind;
    3.24 -val get_kind = the_default "" o try the_kind;
    3.25 +fun get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);
    3.26  
    3.27  fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN;
    3.28  fun kind k x = if k = "" then x else rule_attribute (K (kind_rule k)) x;
    3.29 -fun kind_internal x = kind internalK x;
    3.30 -fun has_internal tags = exists (fn tg => tg = (Markup.kindN, internalK)) tags;
    3.31 -val is_internal = has_internal o Thm.get_tags;
    3.32  
    3.33  
    3.34  open Thm;