src/HOL/Library/Infinite_Set.thy

--- a/src/HOL/Library/Infinite_Set.thy	Thu May 14 10:26:33 2020 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Thu May 14 13:44:44 2020 +0200
@@ -371,8 +371,9 @@
   then show ?case by simp
 next
   case (insert a A)
-  with R show ?case
-    by (metis empty_iff insert_iff)   (* somewhat slow *)
+  have False
+    using R(1)[of a] R(2)[of _ a] insert(3,4) by blast   
+  thus ?case ..
 qed
 
 corollary Union_maximal_sets: