--- a/src/HOLCF/Bifinite.thy Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOLCF/Bifinite.thy Thu Jul 01 16:54:44 2010 +0200
@@ -161,7 +161,7 @@
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed
-instantiation "*" :: (profinite, profinite) profinite
+instantiation prod :: (profinite, profinite) profinite
begin
definition
@@ -187,7 +187,7 @@
end
-instance "*" :: (bifinite, bifinite) bifinite ..
+instance prod :: (bifinite, bifinite) bifinite ..
lemma approx_Pair [simp]:
"approx i\<cdot>(x, y) = (approx i\<cdot>x, approx i\<cdot>y)"