# HG changeset patch # User wenzelm # Date 1256830484 -3600 # Node ID 784c1b09d4851cbf08706eeb2ff1875f5f06edee # Parent 53d49370f7af9d46609cd72c1887c9a5d82eda58 eliminated obsolete/unused Thm.kind_internal/is_internal etc.; diff -r 53d49370f7af -r 784c1b09d485 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu Oct 29 16:15:33 2009 +0100 +++ b/src/Pure/Isar/expression.ML Thu Oct 29 16:34:44 2009 +0100 @@ -641,8 +641,8 @@ |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], []) |> Sign.declare_const ((bname, predT), NoSyn) |> snd |> PureThy.add_defs false - [((Binding.conceal (Binding.map_name Thm.def_name bname), Logic.mk_equals (head, body)), - [Thm.kind_internal])]; + [((Binding.conceal (Binding.map_name Thm.def_name bname), + Logic.mk_equals (head, body)), [])]; val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head; val cert = Thm.cterm_of defs_thy; diff -r 53d49370f7af -r 784c1b09d485 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Thu Oct 29 16:15:33 2009 +0100 +++ b/src/Pure/axclass.ML Thu Oct 29 16:34:44 2009 +0100 @@ -311,7 +311,7 @@ (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const')) #>> Thm.varifyT #-> (fn thm => add_inst_param (c, tyco) (c'', thm) - #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [Thm.kind_internal]) + #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), []) #> snd #> Sign.restore_naming thy #> pair (Const (c, T)))) diff -r 53d49370f7af -r 784c1b09d485 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Thu Oct 29 16:15:33 2009 +0100 +++ b/src/Pure/more_thm.ML Thu Oct 29 16:34:44 2009 +0100 @@ -91,13 +91,9 @@ val lemmaK: string val corollaryK: string val internalK: string - val has_kind: thm -> bool val get_kind: thm -> string val kind_rule: string -> thm -> thm val kind: string -> attribute - val kind_internal: attribute - val has_internal: Properties.property list -> bool - val is_internal: thm -> bool end; structure Thm: THM = @@ -425,16 +421,10 @@ val corollaryK = "corollary"; val internalK = Markup.internalK; -fun the_kind thm = the (Properties.get (Thm.get_tags thm) Markup.kindN); - -val has_kind = can the_kind; -val get_kind = the_default "" o try the_kind; +fun 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; -fun kind_internal x = kind internalK x; -fun has_internal tags = exists (fn tg => tg = (Markup.kindN, internalK)) tags; -val is_internal = has_internal o Thm.get_tags; open Thm;