diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Library/Groups_Big_Fun.thy
--- a/src/HOL/Library/Groups_Big_Fun.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -183,7 +183,7 @@
   have bij: "bij (\<lambda>(a, b, c). ((a, b), c))"
     by (auto intro!: bijI injI simp add: image_def)
   have "{p. \<exists>c. g (fst p) (snd p) c \<noteq> 1} \<times> {c. \<exists>p. g (fst p) (snd p) c \<noteq> 1} \<subseteq> D"
-    by auto (insert subset, auto)
+    by auto (insert subset, blast)
   with fin have "G (\<lambda>p. G (g (fst p) (snd p))) = G (\<lambda>(p, c). g (fst p) (snd p) c)"
     by (rule cartesian_product)
   then have "G (\<lambda>(a, b). G (g a b)) = G (\<lambda>((a, b), c). g a b c)"