--- a/src/HOL/HOLCF/Library/Option_Cpo.thy Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/Library/Option_Cpo.thy Thu Jan 06 16:52:35 2011 -0800
@@ -280,7 +280,7 @@
lemma isodefl_option [domain_isodefl]:
assumes "isodefl' d t"
- shows "isodefl' (option_map d) (sum_liftdefl\<cdot>(pdefl\<cdot>DEFL(unit))\<cdot>t)"
+ shows "isodefl' (option_map d) (sum_liftdefl\<cdot>(liftdefl_of\<cdot>DEFL(unit))\<cdot>t)"
using isodefl_sum [OF isodefl_LIFTDEFL [where 'a=unit] assms]
unfolding isodefl'_def liftemb_option_def liftprj_option_def liftdefl_eq
by (simp add: cfcomp1 u_map_map encode_option_option_map)