diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Cardinal.thy	Tue Oct 01 13:26:10 2002 +0200
@@ -917,8 +917,7 @@
 apply (erule Finite_induct, auto)
 apply (case_tac "x:A")
  apply (subgoal_tac [2] "A-cons (x, B) = A - B")
-apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}")
-apply (rotate_tac -1, simp)
+apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}", simp)
 apply (drule Diff_sing_Finite, auto)
 done