--- a/src/HOL/Algebra/Bij.thy Sun Nov 26 13:19:52 2017 +0100
+++ b/src/HOL/Algebra/Bij.thy Sun Nov 26 21:08:32 2017 +0100
@@ -67,7 +67,7 @@
shows "\<lbrakk>h \<in> Bij S; g \<in> S \<rightarrow> S \<rightarrow> S; x \<in> S; y \<in> S\<rbrakk>
\<Longrightarrow> inv_into S h (g x y) = g (inv_into S h x) (inv_into S h y)"
apply (simp add: Bij_def bij_betw_def)
-apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' & y = h y'", clarify)
+apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' \<and> y = h y'", clarify)
apply (simp add: eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem], blast)
done