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