--- a/src/HOL/Induct/Acc.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Induct/Acc.thy Thu Sep 07 21:10:11 2000 +0200
@@ -18,7 +18,7 @@
inductive "acc r"
intros
- accI [rulify_prems]:
+ accI [rulified]:
"\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r"
syntax