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