src/HOL/Algebra/Ideal.thy

--- a/src/HOL/Algebra/Ideal.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Algebra/Ideal.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -481,7 +481,7 @@
   qed
 next
   show "I <+> J \<subseteq> Idl (I \<union> J)"
-    by (auto simp: set_add_defs genideal_def additive_subgroup.a_closed ideal_def set_mp)
+    by (auto simp: set_add_defs genideal_def additive_subgroup.a_closed ideal_def subsetD)
 qed
 
 subsection \<open>Properties of Principal Ideals\<close>