1.1 --- a/src/HOL/List.thy	Tue Dec 31 22:18:31 2013 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Dec 31 22:18:31 2013 +0100
     1.3 @@ -2822,7 +2822,7 @@
     1.4    "A \<inter> List.coset xs = fold Set.remove xs A"
     1.5    by (simp add: Diff_eq [symmetric] minus_set_fold)
     1.6  
     1.7 -lemma (in semilattice_set) set_eq_fold:
     1.8 +lemma (in semilattice_set) set_eq_fold [code]:
     1.9    "F (set (x # xs)) = fold f xs x"
    1.10  proof -
    1.11    interpret comp_fun_idem f
    1.12 @@ -2830,11 +2830,6 @@
    1.13    show ?thesis by (simp add: eq_fold fold_set_fold)
    1.14  qed
    1.15  
    1.16 -declare Inf_fin.set_eq_fold [code]
    1.17 -declare Sup_fin.set_eq_fold [code]
    1.18 -declare Min.set_eq_fold [code]
    1.19 -declare Max.set_eq_fold [code]
    1.20 -
    1.21  lemma (in complete_lattice) Inf_set_fold:
    1.22    "Inf (set xs) = fold inf xs top"
    1.23  proof -