1.1 --- a/src/HOL/Cardinals/Wellorder_Relation_Base.thy	Wed Apr 24 16:21:23 2013 +0200
     1.2 +++ b/src/HOL/Cardinals/Wellorder_Relation_Base.thy	Wed Apr 24 16:43:19 2013 +0200
     1.3 @@ -234,8 +234,8 @@
     1.4  assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
     1.5  shows "\<exists>b. isMinim B b"
     1.6  proof-
     1.7 -  from WF wf_eq_minimal[of "r - Id"] NE Id_def obtain b where
     1.8 -  *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by force
     1.9 +  from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where
    1.10 +  *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by auto
    1.11    show ?thesis
    1.12    proof(simp add: isMinim_def, rule exI[of _ b], auto)
    1.13      show "b \<in> B" using * by simp