diff -r 1c0b5bfa52a1 -r f432973ce0f6 src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Wed Nov 17 06:49:23 2010 -0800
+++ b/src/HOLCF/Domain.thy	Wed Nov 17 08:47:58 2010 -0800
@@ -237,13 +237,13 @@
 unfolding isodefl_def
 by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb)
 
-lemma isodefl_cfun:
+lemma isodefl_sfun:
   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
-    isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
+    isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
 apply (rule isodeflI)
-apply (simp add: cast_cfun_defl cast_isodefl)
-apply (simp add: emb_cfun_def prj_cfun_def)
-apply (simp add: cfun_map_map cfcomp1)
+apply (simp add: cast_sfun_defl cast_isodefl)
+apply (simp add: emb_sfun_def prj_sfun_def)
+apply (simp add: sfun_map_map isodefl_strict)
 done
 
 lemma isodefl_ssum:
@@ -299,6 +299,23 @@
 apply (simp add: cfcomp1 encode_prod_u_map cast_sprod_defl sprod_map_map)
 done
 
+lemma encode_cfun_map:
+  "encode_cfun\<cdot>(cfun_map\<cdot>f\<cdot>g\<cdot>(decode_cfun\<cdot>x))
+    = sfun_map\<cdot>(u_map\<cdot>f)\<cdot>g\<cdot>x"
+unfolding encode_cfun_def decode_cfun_def
+apply (simp add: sfun_eq_iff cfun_map_def sfun_map_def)
+apply (rule cfun_eqI, rename_tac y, case_tac y, simp_all)
+done
+
+lemma isodefl_cfun:
+  "isodefl (u_map\<cdot>d1) t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
+    isodefl (cfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
+apply (rule isodeflI)
+apply (simp add: cast_sfun_defl cast_isodefl)
+apply (simp add: emb_cfun_def prj_cfun_def encode_cfun_map)
+apply (simp add: sfun_map_map isodefl_strict)
+done
+
 subsection {* Setting up the domain package *}
 
 use "Tools/Domain/domain_isomorphism.ML"
@@ -308,23 +325,24 @@
 setup Domain_Isomorphism.setup
 
 lemmas [domain_defl_simps] =
-  DEFL_cfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
+  DEFL_cfun DEFL_sfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
   liftdefl_eq LIFTDEFL_prod
 
 lemmas [domain_map_ID] =
-  cfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID
+  cfun_map_ID sfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID
 
 lemmas [domain_isodefl] =
-  isodefl_u isodefl_cfun isodefl_ssum isodefl_sprod
-  isodefl_cprod isodefl_cprod_u
+  isodefl_u isodefl_sfun isodefl_ssum isodefl_sprod
+  isodefl_cfun isodefl_cprod isodefl_cprod_u
 
 lemmas [domain_deflation] =
-  deflation_cfun_map deflation_ssum_map deflation_sprod_map
-  deflation_cprod_map deflation_u_map
+  deflation_cfun_map deflation_sfun_map deflation_ssum_map
+  deflation_sprod_map deflation_cprod_map deflation_u_map
 
 setup {*
   fold Domain_Take_Proofs.add_map_function
     [(@{type_name cfun}, @{const_name cfun_map}, [true, true]),
+     (@{type_name "sfun"}, @{const_name sfun_map}, [true, true]),
      (@{type_name ssum}, @{const_name ssum_map}, [true, true]),
      (@{type_name sprod}, @{const_name sprod_map}, [true, true]),
      (@{type_name prod}, @{const_name cprod_map}, [true, true]),