more sort constraints for FinFun code generation

--- a/src/HOL/Library/Cardinality.thy	Sun Jun 03 15:49:55 2012 +0200
+++ b/src/HOL/Library/Cardinality.thy	Mon Jun 04 09:50:57 2012 +0200
@@ -170,9 +170,7 @@
 subsection {* A type class for computing the cardinality of types *}
 
 definition is_list_UNIV :: "'a list \<Rightarrow> bool"
-where "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
-
-lemmas [code_unfold] = is_list_UNIV_def[abs_def]
+where [code del]: "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
 
 lemma is_list_UNIV_iff: "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
 by(auto simp add: is_list_UNIV_def Let_def card_eq_0_iff List.card_set[symmetric] 
@@ -185,6 +183,11 @@
 lemma card_UNIV_code [code_unfold]: "CARD('a :: card_UNIV) = card_UNIV TYPE('a)"
 by(simp add: card_UNIV)
 
+lemma is_list_UNIV_code [code]:
+  "is_list_UNIV (xs :: 'a list) = 
+  (let c = CARD('a :: card_UNIV) in if c = 0 then False else size (remdups xs) = c)"
+by(rule is_list_UNIV_def)
+
 lemma finite_UNIV_conv_card_UNIV [code_unfold]:
   "finite (UNIV :: 'a :: card_UNIV set) \<longleftrightarrow> card_UNIV TYPE('a) > 0"
 by(simp add: card_UNIV card_gt_0_iff)

--- a/src/HOL/Library/FinFun.thy	Sun Jun 03 15:49:55 2012 +0200
+++ b/src/HOL/Library/FinFun.thy	Mon Jun 04 09:50:57 2012 +0200
@@ -435,7 +435,7 @@
 by transfer (simp add: finfun_default_aux_update_const)
 
 lemma finfun_default_const_code [code]:
-  "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = (if CARD('a) = 0 then c else undefined)"
+  "finfun_default ((K$ c) :: 'a :: card_UNIV \<Rightarrow>f 'b) = (if CARD('a) = 0 then c else undefined)"
 by(simp add: finfun_default_const)
 
 lemma finfun_default_update_code [code]: