--- a/src/HOL/Library/Periodic_Fun.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Periodic_Fun.thy Thu Jun 07 19:36:12 2018 +0200
@@ -54,7 +54,7 @@
by (subst of_nat_numeral[symmetric], subst minus_of_nat) (rule refl)
lemma minus_1: "f (gn1 x) = f x"
- using minus_of_nat[of x 1] by (simp add: minus_1_eq minus_eq[symmetric])
+ using minus_of_nat[of x 1] by (simp flip: minus_1_eq minus_eq)
lemmas periodic_simps = plus_of_nat minus_of_nat plus_of_int minus_of_int
plus_numeral minus_numeral plus_1 minus_1