--- a/src/Pure/more_thm.ML Thu Nov 12 21:59:35 2009 +0100
+++ b/src/Pure/more_thm.ML Thu Nov 12 22:02:11 2009 +0100
@@ -91,7 +91,6 @@
val generatedK : string
val lemmaK: string
val corollaryK: string
- val internalK: string
val get_kind: thm -> string
val kind_rule: string -> thm -> thm
val kind: string -> attribute
@@ -421,7 +420,6 @@
val generatedK = "generatedK"
val lemmaK = "lemma";
val corollaryK = "corollary";
-val internalK = Markup.internalK;
fun get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);