--- a/src/HOL/Library/Countable.thy Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Library/Countable.thy Thu Jul 01 16:54:44 2010 +0200
@@ -63,14 +63,14 @@
text {* Pairs *}
-instance "*" :: (countable, countable) countable
+instance prod :: (countable, countable) countable
by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"])
(auto simp add: prod_encode_eq)
text {* Sums *}
-instance "+" :: (countable, countable) countable
+instance sum :: (countable, countable) countable
by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
| Inr b \<Rightarrow> to_nat (True, to_nat b))"])
(simp split: sum.split_asm)