# HG changeset patch
# User blanchet
# Date 1389893857 -3600
# Node ID e40090032de9c2351a160568982175fa6908bd81
# Parent  96b05fd2aee42ddafbb152f09435112ca2450e66
compile (importing 'Metis' or 'Main' would have been an alternative)

diff -r 96b05fd2aee4 -r e40090032de9 src/HOL/Cardinals/Order_Union.thy
--- a/src/HOL/Cardinals/Order_Union.thy	Thu Jan 16 18:26:41 2014 +0100
+++ b/src/HOL/Cardinals/Order_Union.thy	Thu Jan 16 18:37:37 2014 +0100
@@ -31,7 +31,7 @@
     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'"
@@ -59,7 +59,7 @@
     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'"
@@ -338,7 +338,7 @@
     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"
@@ -351,7 +351,7 @@
     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