1.1 --- a/src/HOLCF/ex/Domain_Proofs.thy	Thu Nov 19 15:41:52 2009 -0800
     1.2 +++ b/src/HOLCF/ex/Domain_Proofs.thy	Thu Nov 19 16:47:18 2009 -0800
     1.3 @@ -375,8 +375,8 @@
     1.4      "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
     1.5         'a foo \<rightarrow> 'a foo"
     1.6  where
     1.7 -  "foo_copy = Abs_CFun (\<lambda>(d1, d2, d3). foo_abs oo
     1.8 -        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>d2))
     1.9 +  "foo_copy = (\<Lambda> p. foo_abs oo
    1.10 +        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
    1.11            oo foo_rep)"
    1.12  
    1.13  definition
    1.14 @@ -384,16 +384,16 @@
    1.15      "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
    1.16         'a bar \<rightarrow> 'a bar"
    1.17  where
    1.18 -  "bar_copy = Abs_CFun (\<lambda>(d1, d2, d3). bar_abs oo
    1.19 -        sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>d3) oo bar_rep)"
    1.20 +  "bar_copy = (\<Lambda> p. bar_abs oo
    1.21 +        u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep)"
    1.22  
    1.23  definition
    1.24    baz_copy ::
    1.25      "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
    1.26         'a baz \<rightarrow> 'a baz"
    1.27  where
    1.28 -  "baz_copy = Abs_CFun (\<lambda>(d1, d2, d3). baz_abs oo
    1.29 -        sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(convex_map\<cdot>d1)) oo baz_rep)"
    1.30 +  "baz_copy = (\<Lambda> p. baz_abs oo
    1.31 +        u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep)"
    1.32  
    1.33  definition
    1.34    foo_bar_baz_copy ::
    1.35 @@ -408,10 +408,9 @@
    1.36  apply (subst beta_cfun, simp)+
    1.37  apply (subst pair_collapse)+
    1.38  apply (rule cfun_arg_cong)
    1.39 +unfolding foo_bar_baz_mapF_def split_def
    1.40  unfolding foo_bar_baz_copy_def
    1.41  unfolding foo_copy_def bar_copy_def baz_copy_def
    1.42 -unfolding foo_bar_baz_mapF_def
    1.43 -unfolding split_def
    1.44  apply (subst beta_cfun, simp)+
    1.45  apply (rule refl)
    1.46  done