src/ZF/List.thy

--- a/src/ZF/List.thy	Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/List.thy	Tue Oct 01 13:26:10 2002 +0200
@@ -721,8 +721,7 @@
 apply (induct_tac "m", auto)
 apply (erule_tac a = xs in list.cases)
 apply (auto simp add: take_Nil)
-apply (rotate_tac 1)
-apply (erule natE)
+apply (erule_tac n=n in natE)
 apply (auto intro: take_0 take_type)
 done