# HG changeset patch
# User wenzelm
# Date 1172528308 -3600
# Node ID a9f56907eab7b52f4ac2fd7b4d8fe25dec4066e6
# Parent  6470ce514b6e170ab97c6294a2ef27af220815e7
Thm.internalK;

diff -r 6470ce514b6e -r a9f56907eab7 src/Pure/pure_thy.ML
--- 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;