--- a/doc-src/ZF/ZF_examples.thy	Tue Feb 14 20:57:05 2012 +0100
+++ b/doc-src/ZF/ZF_examples.thy	Tue Feb 14 21:19:39 2012 +0100
@@ -80,7 +80,7 @@
     emptyI:  "0 \<in> Fin(A)"
     consI:   "[| a \<in> A;  b \<in> Fin(A) |] ==> cons(a,b) \<in> Fin(A)"
   type_intros  empty_subsetI cons_subsetI PowI
-  type_elims   PowD [THEN revcut_rl]
+  type_elims   PowD [elim_format]
 
 
 consts  acc :: "i => i"