1.1 --- a/src/HOL/Library/RBT_Set.thy	Tue Nov 05 09:45:00 2013 +0100
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Tue Nov 05 09:45:02 2013 +0100
     1.3 @@ -756,7 +756,8 @@
     1.4  declare Inf_Set_fold[folded Inf'_def, code]
     1.5  
     1.6  lemma INFI_Set_fold [code]:
     1.7 -  "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
     1.8 +  fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
     1.9 +  shows "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
    1.10  proof -
    1.11    have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
    1.12      by default (auto simp add: fun_eq_iff ac_simps)
    1.13 @@ -796,7 +797,8 @@
    1.14  declare Sup_Set_fold[folded Sup'_def, code]
    1.15  
    1.16  lemma SUPR_Set_fold [code]:
    1.17 -  "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
    1.18 +  fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
    1.19 +  shows "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
    1.20  proof -
    1.21    have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
    1.22      by default (auto simp add: fun_eq_iff ac_simps)