# HG changeset patch
# User wenzelm
# Date 1343827956 -7200
# Node ID c028cf680a3e16dda5ac88ab43c8625370a83042
# Parent  81c81f13d15203d92e049da7a9eca79cdd897e36
removed junk;

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