diff -r 51f8a696cd8d -r 9625f3579b48 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Wed Mar 05 21:33:59 2008 +0100
+++ b/src/HOL/Algebra/Coset.thy	Wed Mar 05 21:42:21 2008 +0100
@@ -826,7 +826,7 @@
   includes group G
   shows "H \<in> rcosets H"
 proof -
-  from _ `subgroup H G` have "H #> \<one> = H"
+  from _ subgroup_axioms have "H #> \<one> = H"
     by (rule coset_join2) auto
   then show ?thesis
     by (auto simp add: RCOSETS_def)