diff -r be5b78d95801 -r 562a1d615336 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Wed Mar 26 21:05:58 2008 +0100
+++ b/src/HOLCF/Cprod.thy	Wed Mar 26 22:38:17 2008 +0100
@@ -342,13 +342,13 @@
 
 subsection {* Product type is a bifinite domain *}
 
-instance "*" :: (bifinite_cpo, bifinite_cpo) approx ..
+instance "*" :: (profinite, profinite) approx ..
 
 defs (overloaded)
   approx_cprod_def:
     "approx \<equiv> \<lambda>n. \<Lambda>\<langle>x, y\<rangle>. \<langle>approx n\<cdot>x, approx n\<cdot>y\<rangle>"
 
-instance "*" :: (bifinite_cpo, bifinite_cpo) bifinite_cpo
+instance "*" :: (profinite, profinite) profinite
 proof
   fix i :: nat and x :: "'a \<times> 'b"
   show "chain (\<lambda>i. approx i\<cdot>x)"