diff -r 865bca530d4c -r 04817a8802f2 src/ZF/ex/Group.thy
--- a/src/ZF/ex/Group.thy	Wed Mar 05 14:34:39 2008 +0100
+++ b/src/ZF/ex/Group.thy	Wed Mar 05 21:24:03 2008 +0100
@@ -92,7 +92,7 @@
   assumes inv_ex:
      "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
 
-lemma (in group) is_group [simp]: "group(G)" by fact
+lemma (in group) is_group [simp]: "group(G)" by (rule group_axioms)
 
 theorem groupI:
   includes struct G
@@ -1003,7 +1003,7 @@
   shows "H \<in> rcosets H"
 proof -
   have "H #> \<one> = H"
-    using _ `subgroup(H, G)` by (rule coset_join2) simp_all
+    using _ subgroup_axioms by (rule coset_join2) simp_all
   then show ?thesis
     by (auto simp add: RCOSETS_def intro: sym)
 qed