--- a/src/Pure/pure_thy.ML Mon Feb 26 23:18:27 2007 +0100
+++ b/src/Pure/pure_thy.ML Mon Feb 26 23:18:28 2007 +0100
@@ -140,8 +140,8 @@
fun kind_rule k = tag_rule ("kind", [k]) o untag_rule "kind";
fun kind k x = if k = "" then x else Thm.rule_attribute (K (kind_rule k)) x;
-fun kind_internal x = kind internalK x;
-fun has_internal tags = exists (fn ("kind", [k]) => k = internalK | _ => false) tags;
+fun kind_internal x = kind Thm.internalK x;
+fun has_internal tags = exists (fn ("kind", [k]) => k = Thm.internalK | _ => false) tags;
val is_internal = has_internal o Thm.get_tags;