diff -r f2c9ebbe04aa -r 28cd51cff70c src/HOL/HOLCF/ConvexPD.thy
--- 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