src/HOL/HOLCF/LowerPD.thy

--- 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