1.1 --- a/src/HOL/Finite_Set.thy	Wed Aug 01 12:14:56 2012 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Aug 01 15:32:36 2012 +0200
     1.3 @@ -1788,7 +1788,6 @@
     1.4    with `finite A` have "finite B" by simp
     1.5    interpret fold: folding "op *" "\<lambda>a b. fold (op *) b a" proof
     1.6    qed (simp_all add: fun_eq_iff ac_simps)
     1.7 -  thm fold.comp_fun_commute' [of B b, simplified fun_eq_iff, simplified]
     1.8    from `finite B` fold.comp_fun_commute' [of B x]
     1.9      have "op * x \<circ> (\<lambda>b. fold op * b B) = (\<lambda>b. fold op * b B) \<circ> op * x" by simp
    1.10    then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: fun_eq_iff commute)