diff -r 12585dfb86fe -r 480978f80eae src/HOL/HOLCF/Powerdomains.thy
--- a/src/HOL/HOLCF/Powerdomains.thy	Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/Powerdomains.thy	Thu Jan 06 16:52:35 2011 -0800
@@ -78,7 +78,7 @@
   "(liftprj :: udom u \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::'a upper_pd itself) = pdefl\<cdot>DEFL('a upper_pd)"
+  "liftdefl (t::'a upper_pd itself) = liftdefl_of\<cdot>DEFL('a upper_pd)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
@@ -111,7 +111,7 @@
   "(liftprj :: udom u \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::'a lower_pd itself) = pdefl\<cdot>DEFL('a lower_pd)"
+  "liftdefl (t::'a lower_pd itself) = liftdefl_of\<cdot>DEFL('a lower_pd)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
@@ -144,7 +144,7 @@
   "(liftprj :: udom u \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::'a convex_pd itself) = pdefl\<cdot>DEFL('a convex_pd)"
+  "liftdefl (t::'a convex_pd itself) = liftdefl_of\<cdot>DEFL('a convex_pd)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"