author | wenzelm |
Wed, 31 Oct 2001 01:22:27 +0100 | |
changeset 11993 | d20e653fc64f |
parent 11992 | a39798b57344 |
child 11994 | 319cc9aba0cf |
--- 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;