src/HOL/Cardinals/Order_Union.thy

   show "\<exists>a\<in>A. \<forall>a'\<in>A. (a', a) \<notin> r \<union>o r'"
   proof(cases "B = {}")
     assume Case1: "B \<noteq> {}"
     hence "B \<noteq> {} \<and> B \<le> Field r" using B_def by auto
     then obtain a where 1: "a \<in> B" and 2: "\<forall>a1 \<in> B. (a1,a) \<notin> r"
-    using WF unfolding wf_eq_minimal2 by metis
+    using WF unfolding wf_eq_minimal2 by blast
     hence 3: "a \<in> Field r \<and> a \<notin> Field r'" using B_def FLD by auto
     (*  *)
     have "\<forall>a1 \<in> A. (a1,a) \<notin> r Osum r'"
     proof(intro ballI)
       fix a1 assume **: "a1 \<in> A"

     thus ?thesis using 1 B_def by auto
   next
     assume Case2: "B = {}"
     hence 1: "A \<noteq> {} \<and> A \<le> Field r'" using * ** B_def by auto
     then obtain a' where 2: "a' \<in> A" and 3: "\<forall>a1' \<in> A. (a1',a') \<notin> r'"
-    using WF' unfolding wf_eq_minimal2 by metis
+    using WF' unfolding wf_eq_minimal2 by blast
     hence 4: "a' \<in> Field r' \<and> a' \<notin> Field r" using 1 FLD by blast
     (*  *)
     have "\<forall>a1' \<in> A. (a1',a') \<notin> r Osum r'"
     proof(unfold Osum_def, auto simp add: 3)
       fix a1' assume "(a1', a') \<in> r"

     using FLD unfolding Field_def by blast
     hence "wf((r' - Id) \<union> (Field r \<times> Field r'))"
     using 1 WF' wf_Un[of "Field r \<times> Field r'" "r' - Id"]
     by (auto simp add: Un_commute)
    }
-   ultimately have ?thesis by (metis wf_subset)
+   ultimately have ?thesis using wf_subset by blast
   }
   moreover
   {assume Case22: "r' \<le> Id"
    hence "(r Osum r') - Id \<le> (r - Id) \<union> (Field r \<times> Field r')"
    using Osum_minus_Id2[of r' r] by simp

     using FLD unfolding Field_def by blast
     hence "wf((r - Id) \<union> (Field r \<times> Field r'))"
     using 1 WF wf_Un[of "r - Id" "Field r \<times> Field r'"]
     by (auto simp add: Un_commute)
    }
-   ultimately have ?thesis by (metis wf_subset)
+   ultimately have ?thesis using wf_subset by blast
   }
   ultimately show ?thesis by blast
 qed
 
 lemma Osum_Well_order: