diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Nov 29 17:08:26 2007 +0100
@@ -2689,7 +2689,7 @@
 lemmas [code func] = univ_bool
 
 instance * :: (finite, finite) finite
-  "itself \<equiv> TYPE('a\<Colon>finite)"
+  "itself \<equiv> TYPE('a \<times> 'b)"
 proof
   show "finite (UNIV :: ('a \<times> 'b) set)"
   proof (rule finite_Prod_UNIV)
@@ -2703,7 +2703,7 @@
   unfolding UNIV_Times_UNIV ..
 
 instance "+" :: (finite, finite) finite
-  "itself \<equiv> TYPE('a\<Colon>finite + 'b\<Colon>finite)"
+  "itself \<equiv> TYPE('a + 'b)"
 proof
   have a: "finite (UNIV :: 'a set)" by (rule finite)
   have b: "finite (UNIV :: 'b set)" by (rule finite)
@@ -2717,7 +2717,7 @@
   unfolding UNIV_Plus_UNIV ..
 
 instance set :: (finite) finite
-  "itself \<equiv> TYPE('a\<Colon>finite set)"
+  "itself \<equiv> TYPE('a set)"
 proof
   have "finite (UNIV :: 'a set)" by (rule finite)
   hence "finite (Pow (UNIV :: 'a set))"
@@ -2732,7 +2732,7 @@
   by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
 
 instance "fun" :: (finite, finite) finite
-  "itself \<equiv> TYPE('a\<Colon>finite \<Rightarrow> 'b\<Colon>finite)"
+  "itself \<equiv> TYPE('a \<Rightarrow> 'b)"
 proof
   show "finite (UNIV :: ('a => 'b) set)"
   proof (rule finite_imageD)