src/HOLCF/Cprod.thy

   approx_cprod_def:
     "approx = (\<lambda>n. \<Lambda>\<langle>x, y\<rangle>. \<langle>approx n\<cdot>x, approx n\<cdot>y\<rangle>)"
 
 instance proof
   fix i :: nat and x :: "'a \<times> 'b"
-  show "chain (\<lambda>i. approx i\<cdot>x)"
+  show "chain (approx :: nat \<Rightarrow> 'a \<times> 'b \<rightarrow> 'a \<times> 'b)"
     unfolding approx_cprod_def by simp
   show "(\<Squnion>i. approx i\<cdot>x) = x"
     unfolding approx_cprod_def
     by (simp add: lub_distribs eta_cfun)
   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"