src/HOL/Algebra/Sylow.thy

--- a/src/HOL/Algebra/Sylow.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Wed May 07 10:57:19 2008 +0200
@@ -262,7 +262,7 @@
 apply (rule coset_join1 [THEN in_H_imp_eq])
 apply (rule_tac [3] H_is_subgroup)
 prefer 2 apply (blast intro: m_closed M_elem_map_carrier inv_closed)
-apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_def)
+apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_eq)
 done