diff -r 8df4c332cb1c -r 6a80fbc4e72c src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Tue Sep 13 13:17:52 2011 +0200
+++ b/src/HOL/Big_Operators.thy	Tue Sep 13 16:21:48 2011 +0200
@@ -1433,11 +1433,10 @@
 proof -
   interpret ab_semigroup_idem_mult inf
     by (rule ab_semigroup_idem_mult_inf)
-  from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
+  from `A \<noteq> {}` obtain b B where "A = {b} \<union> B" by auto
   moreover with `finite A` have "finite B" by simp
-  ultimately show ?thesis  
-  by (simp add: Inf_fin_def fold1_eq_fold_idem inf_Inf_fold_inf [symmetric])
-    (simp add: Inf_fold_inf)
+  ultimately show ?thesis
+    by (simp add: Inf_fin_def fold1_eq_fold_idem inf_Inf_fold_inf [symmetric])
 qed
 
 lemma Sup_fin_Sup:
@@ -1446,11 +1445,10 @@
 proof -
   interpret ab_semigroup_idem_mult sup
     by (rule ab_semigroup_idem_mult_sup)
-  from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
+  from `A \<noteq> {}` obtain b B where "A = {b} \<union> B" by auto
   moreover with `finite A` have "finite B" by simp
   ultimately show ?thesis  
   by (simp add: Sup_fin_def fold1_eq_fold_idem sup_Sup_fold_sup [symmetric])
-    (simp add: Sup_fold_sup)
 qed
 
 end