diff -r 9722171731af -r f88b187ad8ca src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Mon Feb 27 20:55:30 2012 +0100
+++ b/src/HOL/Algebra/Coset.thy	Mon Feb 27 21:07:00 2012 +0100
@@ -232,7 +232,7 @@
   also from carr
       have "\<dots> = x' \<otimes> ((inv x) \<otimes> x)" by (simp add: m_assoc)
   also from carr
-      have "\<dots> = x' \<otimes> \<one>" by (simp add: l_inv)
+      have "\<dots> = x' \<otimes> \<one>" by simp
   also from carr
       have "\<dots> = x'" by simp
   finally
@@ -520,8 +520,7 @@
 apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
 apply (rule_tac x = x in bexI)
 apply (rule bexI [of _ "\<one>"])
-apply (auto simp add: subgroup.m_closed subgroup.one_closed
-                      r_one subgroup.subset [THEN subsetD])
+apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD])
 done
 
 
@@ -612,7 +611,7 @@
       fix x y
       assume [simp]: "x \<in> carrier G" "y \<in> carrier G" 
          and "inv x \<otimes> y \<in> H"
-      hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed) 
+      hence "inv (inv x \<otimes> y) \<in> H" by simp
       thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
     qed
   next
@@ -722,7 +721,7 @@
   assume abrcong: "(a, b) \<in> rcong H"
     and ccarr: "c \<in> carrier G"
 
-  from ccarr have "c \<in> Units G" by (simp add: Units_eq)
+  from ccarr have "c \<in> Units G" by simp
   hence cinvc_one: "inv c \<otimes> c = \<one>" by (rule Units_l_inv)
 
   from abrcong