src/HOL/Algebra/Sylow.thy

--- a/src/HOL/Algebra/Sylow.thy	Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Algebra/Sylow.thy	Wed Mar 25 10:44:57 2015 +0100
@@ -182,7 +182,7 @@
 apply (erule H_into_carrier_G)
 apply (rule H_not_empty)
 apply (simp add: H_def, clarify)
-apply (erule_tac P = "%z. ?lhs(z) = M1" in subst)
+apply (erule_tac P = "%z. lhs(z) = M1" for lhs in subst)
 apply (simp add: coset_mult_assoc )
 apply (blast intro: H_m_closed)
 done