# HG changeset patch
# User wenzelm
# Date 1004487747 -3600
# Node ID d20e653fc64fd4bcbf41628a894132cc1dfee8d8
# Parent  a39798b573441c0fe2c8a2bf8572d6991b5acffc
put_consumes: really overwrite existing tag;

diff -r a39798b57344 -r d20e653fc64f src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Wed Oct 31 01:21:56 2001 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Wed Oct 31 01:22:27 2001 +0100
@@ -43,7 +43,8 @@
     | _ => err ())
   end;
 
-fun put_consumes n = Drule.tag_rule (consumes_tagN, [Library.string_of_int n]);
+fun put_consumes n =
+  Drule.tag_rule (consumes_tagN, [Library.string_of_int n]) o Drule.untag_rule consumes_tagN;
 val save_consumes = put_consumes o get_consumes;
 
 fun consumes n x = Drule.rule_attribute (K (put_consumes n)) x;