--- a/src/HOL/HOLCF/Algebraic.thy Wed Dec 01 06:50:54 2010 -0800
+++ b/src/HOL/HOLCF/Algebraic.thy Wed Dec 01 20:29:39 2010 -0800
@@ -73,7 +73,7 @@
subsection {* Defining algebraic deflations by ideal completion *}
typedef (open) defl = "{S::fin_defl set. below.ideal S}"
-by (fast intro: below.ideal_principal)
+by (rule below.ex_ideal)
instantiation defl :: below
begin
--- a/src/HOL/HOLCF/Completion.thy Wed Dec 01 06:50:54 2010 -0800
+++ b/src/HOL/HOLCF/Completion.thy Wed Dec 01 20:29:39 2010 -0800
@@ -49,8 +49,8 @@
apply (fast intro: r_trans)
done
-lemma ex_ideal: "\<exists>A. ideal A"
-by (rule exI, rule ideal_principal)
+lemma ex_ideal: "\<exists>A. A \<in> {A. ideal A}"
+by (fast intro: ideal_principal)
lemma lub_image_principal:
assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
--- a/src/HOL/HOLCF/ConvexPD.thy Wed Dec 01 06:50:54 2010 -0800
+++ b/src/HOL/HOLCF/ConvexPD.thy Wed Dec 01 20:29:39 2010 -0800
@@ -121,7 +121,7 @@
typedef (open) 'a convex_pd =
"{S::'a pd_basis set. convex_le.ideal S}"
-by (fast intro: convex_le.ideal_principal)
+by (rule convex_le.ex_ideal)
instantiation convex_pd :: ("domain") below
begin
--- a/src/HOL/HOLCF/LowerPD.thy Wed Dec 01 06:50:54 2010 -0800
+++ b/src/HOL/HOLCF/LowerPD.thy Wed Dec 01 20:29:39 2010 -0800
@@ -76,7 +76,7 @@
typedef (open) 'a lower_pd =
"{S::'a pd_basis set. lower_le.ideal S}"
-by (fast intro: lower_le.ideal_principal)
+by (rule lower_le.ex_ideal)
instantiation lower_pd :: ("domain") below
begin
--- a/src/HOL/HOLCF/Universal.thy Wed Dec 01 06:50:54 2010 -0800
+++ b/src/HOL/HOLCF/Universal.thy Wed Dec 01 20:29:39 2010 -0800
@@ -199,7 +199,7 @@
subsection {* Defining the universal domain by ideal completion *}
typedef (open) udom = "{S. udom.ideal S}"
-by (fast intro: udom.ideal_principal)
+by (rule udom.ex_ideal)
instantiation udom :: below
begin
--- a/src/HOL/HOLCF/UpperPD.thy Wed Dec 01 06:50:54 2010 -0800
+++ b/src/HOL/HOLCF/UpperPD.thy Wed Dec 01 20:29:39 2010 -0800
@@ -74,7 +74,7 @@
typedef (open) 'a upper_pd =
"{S::'a pd_basis set. upper_le.ideal S}"
-by (fast intro: upper_le.ideal_principal)
+by (rule upper_le.ex_ideal)
instantiation upper_pd :: ("domain") below
begin