src/Pure/drule.ML
changeset 8365 affb2989d238
parent 8328 efbcec3eb02f
child 8406 a217b0cd304d
     1.1 --- a/src/Pure/drule.ML	Wed Mar 08 17:48:31 2000 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Mar 08 17:49:28 2000 +0100
     1.3 @@ -98,6 +98,8 @@
     1.4    val unvarifyT         : thm -> thm
     1.5    val unvarify          : thm -> thm
     1.6    val rule_attribute    : ('a -> thm -> thm) -> 'a attribute
     1.7 +  val tag_rule          : tag -> thm -> thm
     1.8 +  val untag_rule        : tag -> thm -> thm
     1.9    val tag               : tag -> 'a attribute
    1.10    val untag             : tag -> 'a attribute
    1.11    val tag_lemma         : 'a attribute
    1.12 @@ -749,8 +751,11 @@
    1.13  fun map_tags f thm =
    1.14    Thm.put_name_tags (Thm.name_of_thm thm, f (#2 (Thm.get_name_tags thm))) thm;
    1.15  
    1.16 -fun tag tg x = rule_attribute (K (map_tags (fn tgs => if tg mem tgs then tgs else tgs @ [tg]))) x;
    1.17 -fun untag tg x = rule_attribute (K (map_tags (fn tgs => tgs \ tg))) x;
    1.18 +fun tag_rule tg = map_tags (fn tgs => if tg mem tgs then tgs else tgs @ [tg]);
    1.19 +fun untag_rule tg = map_tags (fn tgs => tgs \ tg);
    1.20 +
    1.21 +fun tag tg x = rule_attribute (K (tag_rule tg)) x;
    1.22 +fun untag tg x = rule_attribute (K (untag_rule tg)) x;
    1.23  
    1.24  fun simple_tag name x = tag (name, []) x;
    1.25