src/HOL/Library/FinFun.thy
changeset 48070 02d64fd40852
parent 48059 f6ce99d3719b
child 48100 0122ba071e1a
     1.1 --- a/src/HOL/Library/FinFun.thy	Sun Jun 03 15:49:55 2012 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Mon Jun 04 09:50:57 2012 +0200
     1.3 @@ -435,7 +435,7 @@
     1.4  by transfer (simp add: finfun_default_aux_update_const)
     1.5  
     1.6  lemma finfun_default_const_code [code]:
     1.7 -  "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = (if CARD('a) = 0 then c else undefined)"
     1.8 +  "finfun_default ((K$ c) :: 'a :: card_UNIV \<Rightarrow>f 'b) = (if CARD('a) = 0 then c else undefined)"
     1.9  by(simp add: finfun_default_const)
    1.10  
    1.11  lemma finfun_default_update_code [code]: