# HG changeset patch
# User wenzelm
# Date 953306939 -3600
# Node ID 7e4a466b18d581b45586ec949d9126fe58a0ad36
# Parent  4f5a3272c8ba3b572b31dcf08592e16ca913fa22
untag: remove all tags of given name;

diff -r 4f5a3272c8ba -r 7e4a466b18d5 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Mar 17 16:27:28 2000 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Mar 17 16:28:59 2000 +0100
@@ -169,7 +169,7 @@
 (* tags *)
 
 fun gen_tag x = syntax (tag >> Drule.tag) x;
-fun gen_untag x = syntax (tag >> Drule.untag) x;
+fun gen_untag x = syntax (Scan.lift Args.name >> Drule.untag) x;
 
 
 (* transfer *)
diff -r 4f5a3272c8ba -r 7e4a466b18d5 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Mar 17 16:27:28 2000 +0100
+++ b/src/Pure/drule.ML	Fri Mar 17 16:28:59 2000 +0100
@@ -99,9 +99,9 @@
   val unvarify          : thm -> thm
   val rule_attribute    : ('a -> thm -> thm) -> 'a attribute
   val tag_rule          : tag -> thm -> thm
-  val untag_rule        : tag -> thm -> thm
+  val untag_rule        : string -> thm -> thm
   val tag               : tag -> 'a attribute
-  val untag             : tag -> 'a attribute
+  val untag             : string -> 'a attribute
   val tag_lemma         : 'a attribute
   val tag_assumption    : 'a attribute
   val tag_internal      : 'a attribute
@@ -752,10 +752,10 @@
   Thm.put_name_tags (Thm.name_of_thm thm, f (#2 (Thm.get_name_tags thm))) thm;
 
 fun tag_rule tg = map_tags (fn tgs => if tg mem tgs then tgs else tgs @ [tg]);
-fun untag_rule tg = map_tags (fn tgs => tgs \ tg);
+fun untag_rule s = map_tags (filter_out (equal s o #1));
 
 fun tag tg x = rule_attribute (K (tag_rule tg)) x;
-fun untag tg x = rule_attribute (K (untag_rule tg)) x;
+fun untag s x = rule_attribute (K (untag_rule s)) x;
 
 fun simple_tag name x = tag (name, []) x;