changeset 45375 | 7fe19930dfc9 |
parent 42817 | 7e819eb7dabb |
child 46459 | 73823dbbecc4 |
--- a/src/Provers/classical.ML Sun Nov 06 21:17:45 2011 +0100 +++ b/src/Provers/classical.ML Sun Nov 06 21:51:46 2011 +0100 @@ -848,7 +848,11 @@ val haz_elim = attrib o addE; val haz_intro = attrib o addI; val haz_dest = attrib o addD; -val rule_del = attrib delrule o Context_Rules.rule_del; + +val rule_del = + Thm.declaration_attribute (fn th => fn context => + context |> map_cs (delrule (SOME context) th) |> + Thm.attribute_declaration Context_Rules.rule_del th);