--- a/src/HOL/Algebra/Sym_Groups.thy Mon Sep 10 21:33:14 2018 +0200
+++ b/src/HOL/Algebra/Sym_Groups.thy Tue Sep 11 16:21:54 2018 +0100
@@ -339,7 +339,7 @@
proof (intro nth_equalityI)
show "length cs = length [(cs ! 0), (cs ! 1), (cs ! 2)]"
using assms by simp
- show "\<forall> ia < length cs. cs ! ia = [(cs ! 0), (cs ! 1), (cs ! 2)] ! ia"
+ show "\<And>i. i < length cs \<Longrightarrow> cs ! i = [(cs ! 0), (cs ! 1), (cs ! 2)] ! i"
by (metis Suc_1 Suc_eq_plus1 add.left_neutral assms less_antisym
less_one nth_Cons' nth_Cons_Suc numeral_3_eq_3)
qed