src/HOL/HOLCF/UpperPD.thy

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