diff -r c7699379a72f -r 4953e21ac76c src/HOL/HOLCF/Library/List_Predomain.thy
--- a/src/HOL/HOLCF/Library/List_Predomain.thy	Mon Dec 20 09:45:26 2010 +0100
+++ b/src/HOL/HOLCF/Library/List_Predomain.thy	Mon Dec 20 07:50:47 2010 -0800
@@ -143,33 +143,23 @@
   "LIFTDEFL('a::predomain list) = list_liftdefl\<cdot>LIFTDEFL('a)"
 by (rule liftdefl_list_def)
 
-subsection {* Continuous map operation for lists *}
-
-definition
-  list_map :: "('a::predomain \<rightarrow> 'b::predomain) \<rightarrow> 'a list \<rightarrow> 'b list"
-where
-  "list_map = (\<Lambda> f xs. map (\<lambda>x. f\<cdot>x) xs)"
+subsection {* Configuring list type to work with domain package *}
 
-lemma list_map_simps [simp]:
-  "list_map\<cdot>f\<cdot>[] = []"
-  "list_map\<cdot>f\<cdot>(x # xs) = f\<cdot>x # list_map\<cdot>f\<cdot>xs"
-unfolding list_map_def by simp_all
+abbreviation list_map :: "('a::cpo \<rightarrow> 'b::cpo) \<Rightarrow> 'a list \<rightarrow> 'b list"
+  where "list_map f \<equiv> Abs_cfun (map (Rep_cfun f))"
 
-lemma list_map_ID [domain_map_ID]: "list_map\<cdot>ID = ID"
-unfolding list_map_def ID_def
-by (simp add: Abs_cfun_inverse cfun_def)
+lemma list_map_ID [domain_map_ID]: "list_map ID = ID"
+by (simp add: ID_def cfun_eq_iff Abs_cfun_inverse2)
 
 lemma deflation_list_map [domain_deflation]:
-  "deflation d \<Longrightarrow> deflation (list_map\<cdot>d)"
+  "deflation d \<Longrightarrow> deflation (list_map d)"
 apply default
 apply (induct_tac x, simp_all add: deflation.idem)
 apply (induct_tac x, simp_all add: deflation.below)
 done
 
-subsection {* Configuring list type to work with domain package *}
-
 lemma encode_list_u_map:
-  "encode_list_u\<cdot>(u_map\<cdot>(list_map\<cdot>f)\<cdot>(decode_list_u\<cdot>xs))
+  "encode_list_u\<cdot>(u_map\<cdot>(list_map f)\<cdot>(decode_list_u\<cdot>xs))
     = slist_map\<cdot>(u_map\<cdot>f)\<cdot>xs"
 apply (induct xs, simp, simp)
 apply (case_tac a, simp, rename_tac b)
@@ -180,7 +170,7 @@
 lemma isodefl_list_u [domain_isodefl]:
   fixes d :: "'a::predomain \<rightarrow> 'a"
   assumes "isodefl' d t"
-  shows "isodefl' (list_map\<cdot>d) (list_liftdefl\<cdot>t)"
+  shows "isodefl' (list_map d) (list_liftdefl\<cdot>t)"
 using assms unfolding isodefl'_def liftemb_list_def liftprj_list_def
 apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_defl)
 apply (simp add: cfcomp1 encode_list_u_map)