src/HOL/HOLCF/Universal.thy

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