diff -r e99fd663c4a3 -r 7fe19930dfc9 src/Provers/classical.ML
--- 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);