untag: remove all tags of given name;
authorwenzelm
Fri Mar 17 16:28:59 2000 +0100 (2000-03-17)
changeset 84967e4a466b18d5
parent 8495 4f5a3272c8ba
child 8497 88d7a4f834ff
untag: remove all tags of given name;
src/Pure/Isar/attrib.ML
src/Pure/drule.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Fri Mar 17 16:27:28 2000 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Fri Mar 17 16:28:59 2000 +0100
     1.3 @@ -169,7 +169,7 @@
     1.4  (* tags *)
     1.5  
     1.6  fun gen_tag x = syntax (tag >> Drule.tag) x;
     1.7 -fun gen_untag x = syntax (tag >> Drule.untag) x;
     1.8 +fun gen_untag x = syntax (Scan.lift Args.name >> Drule.untag) x;
     1.9  
    1.10  
    1.11  (* transfer *)
     2.1 --- a/src/Pure/drule.ML	Fri Mar 17 16:27:28 2000 +0100
     2.2 +++ b/src/Pure/drule.ML	Fri Mar 17 16:28:59 2000 +0100
     2.3 @@ -99,9 +99,9 @@
     2.4    val unvarify          : thm -> thm
     2.5    val rule_attribute    : ('a -> thm -> thm) -> 'a attribute
     2.6    val tag_rule          : tag -> thm -> thm
     2.7 -  val untag_rule        : tag -> thm -> thm
     2.8 +  val untag_rule        : string -> thm -> thm
     2.9    val tag               : tag -> 'a attribute
    2.10 -  val untag             : tag -> 'a attribute
    2.11 +  val untag             : string -> 'a attribute
    2.12    val tag_lemma         : 'a attribute
    2.13    val tag_assumption    : 'a attribute
    2.14    val tag_internal      : 'a attribute
    2.15 @@ -752,10 +752,10 @@
    2.16    Thm.put_name_tags (Thm.name_of_thm thm, f (#2 (Thm.get_name_tags thm))) thm;
    2.17  
    2.18  fun tag_rule tg = map_tags (fn tgs => if tg mem tgs then tgs else tgs @ [tg]);
    2.19 -fun untag_rule tg = map_tags (fn tgs => tgs \ tg);
    2.20 +fun untag_rule s = map_tags (filter_out (equal s o #1));
    2.21  
    2.22  fun tag tg x = rule_attribute (K (tag_rule tg)) x;
    2.23 -fun untag tg x = rule_attribute (K (untag_rule tg)) x;
    2.24 +fun untag s x = rule_attribute (K (untag_rule s)) x;
    2.25  
    2.26  fun simple_tag name x = tag (name, []) x;
    2.27