diff -r 5a9081c3b869 -r 8035a13c61a0 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Sep 07 20:56:04 2000 +0200
+++ b/src/Pure/Isar/method.ML	Thu Sep 07 20:56:58 2000 +0200
@@ -203,10 +203,14 @@
 (* concrete syntax *)
 
 val rule_atts =
- [("dest", (Attrib.no_args dest_global, Attrib.no_args dest_local), "declare destruction rule"),
-  ("elim", (Attrib.no_args elim_global, Attrib.no_args elim_local), "declare elimination rule"),
-  ("intro", (Attrib.no_args intro_global, Attrib.no_args intro_local), "declare introduction rule"),
-  ("delrule", (Attrib.no_args delrule_global, Attrib.no_args delrule_local), "undeclare rule")];
+ [("dest", (Attrib.no_args dest_global, Attrib.no_args dest_local),
+    "declaration of destruction rule"),
+  ("elim", (Attrib.no_args elim_global, Attrib.no_args elim_local),
+    "declaration of elimination rule"),
+  ("intro", (Attrib.no_args intro_global, Attrib.no_args intro_local),
+    "declaration of introduction rule"),
+  ("delrule", (Attrib.no_args delrule_global, Attrib.no_args delrule_local),
+    "remove declaration of elim/intro rule")];