removed kind attribs;

--- a/src/Pure/Isar/attrib.ML	Tue Nov 21 18:07:35 2006 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Nov 21 18:07:36 2006 +0100
@@ -35,11 +35,6 @@
     attribute * (Context.generic * Args.T list)) -> src -> attribute
   val no_args: attribute -> src -> attribute
   val add_del_args: attribute -> attribute -> src -> attribute
-  val kind: string -> src
-  val kind_theorem: src
-  val kind_lemma: src
-  val kind_corollary: src
-  val kind_internal: src
   val internal: attribute -> src
 end;
 
@@ -207,16 +202,7 @@
 fun tagged x = syntax (tag >> PureThy.tag) x;
 fun untagged x = syntax (Scan.lift Args.name >> PureThy.untag) x;
 
-
-(* kinds *)
-
-fun kind_att x = syntax (Scan.lift Args.name >> PureThy.kind) x;
-fun kind name = Args.src (("Pure.kind", [Args.mk_string (name, Position.none)]), Position.none);
-
-val kind_theorem = kind PureThy.theoremK;
-val kind_lemma = kind PureThy.lemmaK;
-val kind_corollary = kind PureThy.corollaryK;
-val kind_internal = kind PureThy.internalK;
+fun kind x = syntax (Scan.lift Args.name >> PureThy.kind) x;
 
 
 (* rule composition *)
@@ -290,7 +276,7 @@
  (add_attributes
    [("tagged", tagged, "tagged theorem"),
     ("untagged", untagged, "untagged theorem"),
-    ("kind", kind_att, "theorem kind"),
+    ("kind", kind, "theorem kind"),
     ("COMP", COMP_att, "direct composition with rules (no lifting)"),
     ("THEN", THEN_att, "resolution with rule"),
     ("OF", OF_att, "rule applied to facts"),