diff -r 102f2430cef9 -r fe05af7ec816 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Sep 12 22:13:23 2000 +0200
@@ -269,7 +269,7 @@
 (* misc rules *)
 
 fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x;
-fun elimified x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x;
+fun elim_format x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x;
 fun no_vars x = no_args (Drule.rule_attribute (K (#1 o Drule.freeze_thaw))) x;
 
 fun exported_global x = no_args (Drule.rule_attribute (Proof.export_thm o ProofContext.init)) x;
@@ -292,7 +292,7 @@
   ("unfolded", (unfolded_global, unfolded_local), "unfolded definitions"),
   ("folded", (folded_global, folded_local), "folded definitions"),
   ("standard", (standard, standard), "result put into standard form"),
-  ("elimified", (elimified, elimified), "destruct rule turned into elimination rule"),
+  ("elim_format", (elim_format, elim_format), "destruct rule turned into elimination rule format"),
   ("no_vars", (no_vars, no_vars), "frozen schematic vars"),
   ("case_names", (case_names, case_names), "named rule cases"),
   ("params", (params, params), "named rule parameters"),