diff -r fcd5af4aac2b -r 7c59fe17f495 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Sat Mar 30 14:57:06 2013 +0100
+++ b/src/HOL/Big_Operators.thy	Fri Mar 29 18:57:47 2013 +0100
@@ -1417,7 +1417,7 @@
   then show ?thesis by (simp add: * insert_commute)
 qed
 
-lemma subsumption:
+lemma in_idem:
   assumes "finite A" and "x \<in> A"
   shows "x * F A = F A"
 proof -
@@ -1429,7 +1429,7 @@
 lemma insert [simp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "F (insert x A) = x * F A"
-  using assms by (cases "x \<in> A") (simp_all add: insert_absorb subsumption insert_not_elem)
+  using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem)
 
 lemma union:
   assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
@@ -1564,7 +1564,7 @@
   from assms show ?thesis by (simp add: eq_fold)
 qed
 
-lemma subsumption:
+lemma in_idem:
   assumes "finite A" and "x \<in> A"
   shows "x * F A = F A"
 proof -