removed kind attribs;
authorwenzelm
Tue Nov 21 18:07:36 2006 +0100 (2006-11-21)
changeset 21439303ec9e9f74f
parent 21438 90dda96bca98
child 21440 807a39221a58
removed kind attribs;
src/Pure/Isar/attrib.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Tue Nov 21 18:07:35 2006 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Tue Nov 21 18:07:36 2006 +0100
     1.3 @@ -35,11 +35,6 @@
     1.4      attribute * (Context.generic * Args.T list)) -> src -> attribute
     1.5    val no_args: attribute -> src -> attribute
     1.6    val add_del_args: attribute -> attribute -> src -> attribute
     1.7 -  val kind: string -> src
     1.8 -  val kind_theorem: src
     1.9 -  val kind_lemma: src
    1.10 -  val kind_corollary: src
    1.11 -  val kind_internal: src
    1.12    val internal: attribute -> src
    1.13  end;
    1.14  
    1.15 @@ -207,16 +202,7 @@
    1.16  fun tagged x = syntax (tag >> PureThy.tag) x;
    1.17  fun untagged x = syntax (Scan.lift Args.name >> PureThy.untag) x;
    1.18  
    1.19 -
    1.20 -(* kinds *)
    1.21 -
    1.22 -fun kind_att x = syntax (Scan.lift Args.name >> PureThy.kind) x;
    1.23 -fun kind name = Args.src (("Pure.kind", [Args.mk_string (name, Position.none)]), Position.none);
    1.24 -
    1.25 -val kind_theorem = kind PureThy.theoremK;
    1.26 -val kind_lemma = kind PureThy.lemmaK;
    1.27 -val kind_corollary = kind PureThy.corollaryK;
    1.28 -val kind_internal = kind PureThy.internalK;
    1.29 +fun kind x = syntax (Scan.lift Args.name >> PureThy.kind) x;
    1.30  
    1.31  
    1.32  (* rule composition *)
    1.33 @@ -290,7 +276,7 @@
    1.34   (add_attributes
    1.35     [("tagged", tagged, "tagged theorem"),
    1.36      ("untagged", untagged, "untagged theorem"),
    1.37 -    ("kind", kind_att, "theorem kind"),
    1.38 +    ("kind", kind, "theorem kind"),
    1.39      ("COMP", COMP_att, "direct composition with rules (no lifting)"),
    1.40      ("THEN", THEN_att, "resolution with rule"),
    1.41      ("OF", OF_att, "rule applied to facts"),