--- a/src/HOL/GroupTheory/Coset.thy	Mon Oct 07 19:01:51 2002 +0200
+++ b/src/HOL/GroupTheory/Coset.thy	Tue Oct 08 08:20:17 2002 +0200
@@ -345,7 +345,6 @@
 apply (rule inj_onI)
 apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
  prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
-apply (rotate_tac -1)
 apply (simp add: subsetD)
 done