src/HOL/Algebra/AbelCoset.thy

--- a/src/HOL/Algebra/AbelCoset.thy	Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy	Wed Feb 17 21:51:56 2016 +0100
@@ -258,7 +258,7 @@
     from a_subgroup have Hcarr: "H \<subseteq> carrier G"
       unfolding subgroup_def by simp
     from xcarr Hcarr show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
-      using m_comm [simplified] by fast
+      using m_comm [simplified] by fastforce
   qed
 qed