src/HOL/Algebra/Divisibility.thy

   then show ?case
     by simp (meson Units_one_closed aprime carr divides_unit primeE)
 next
   case (Cons x as)
   then have "x \<in> carrier G"  "set as \<subseteq> carrier G" and "a divides x \<otimes> foldr (\<otimes>) as \<one>"
-    by (auto simp: )
+    by auto
   with carr aprime have "a divides x \<or> a divides foldr (\<otimes>) as \<one>"
     by (intro prime_divides) simp+
   then show ?case
     using Cons.IH Cons.prems(1) by force
 qed