diff -r b9dd40e2c470 -r e4d5a07fecb6 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Nov 11 14:34:02 2018 +0100
+++ b/src/HOL/Finite_Set.thy	Sun Nov 11 16:08:59 2018 +0100
@@ -291,7 +291,7 @@
   from B_A \<open>x \<notin> B\<close> have "B = f ` A - {x}"
     by blast
   with B_A \<open>x \<notin> B\<close> \<open>x = f y\<close> \<open>inj_on f A\<close> \<open>y \<in> A\<close> have "B = f ` (A - {y})"
-    by (simp add: inj_on_image_set_diff Set.Diff_subset)
+    by (simp add: inj_on_image_set_diff)
   moreover from \<open>inj_on f A\<close> have "inj_on f (A - {y})"
     by (rule inj_on_diff)
   ultimately have "finite (A - {y})"