--- a/src/HOL/Induct/Acc.thy Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Induct/Acc.thy Tue Sep 12 22:13:23 2000 +0200
@@ -18,7 +18,7 @@
inductive "acc r"
intros
- accI [rulified]:
+ accI [rule_format]:
"\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r"
syntax