diff -r a08e916f4946 -r 28b5eb4a867f src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Wed May 19 11:29:47 2004 +0200
+++ b/src/HOL/Algebra/Coset.thy	Wed May 19 11:30:18 2004 +0200
@@ -502,8 +502,7 @@
 lemma (in group) inv_FactGroup:
      "N <| G ==> X \<in> carrier (G Mod N) ==> inv\<^bsub>G Mod N\<^esub> X = set_inv G X"
 apply (rule group.inv_equality [OF factorgroup_is_group]) 
-apply (simp_all add: FactGroup_def setinv_closed 
-    setrcos_inv_mult_group_eq group.intro [OF prems])
+apply (simp_all add: FactGroup_def setinv_closed setrcos_inv_mult_group_eq)
 done
 
 text{*The coset map is a homomorphism from @{term G} to the quotient group
@@ -511,7 +510,6 @@
 lemma (in group) r_coset_hom_Mod:
   assumes N: "N <| G"
   shows "(r_coset G N) \<in> hom G (G Mod N)"
-by (simp add: FactGroup_def rcosets_def Pi_def hom_def
-           rcos_sum group.intro prems) 
+by (simp add: FactGroup_def rcosets_def Pi_def hom_def rcos_sum N) 
 
 end