diff -r 691c02d1699b -r 223172b97d0b src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Wed Jun 06 13:04:52 2018 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Wed Jun 06 18:19:55 2018 +0200
@@ -1148,8 +1148,7 @@
 lemma Gamma_1 [simp]: "Gamma 1 = 1" unfolding Gamma_def by simp
 
 lemma Gamma_fact: "Gamma (1 + of_nat n) = fact n"
-  by (simp add: pochhammer_fact pochhammer_Gamma of_nat_in_nonpos_Ints_iff
-        reorient: of_nat_Suc)
+  by (simp add: pochhammer_fact pochhammer_Gamma of_nat_in_nonpos_Ints_iff flip: of_nat_Suc)
 
 lemma Gamma_numeral: "Gamma (numeral n) = fact (pred_numeral n)"
   by (subst of_nat_numeral[symmetric], subst numeral_eq_Suc,
@@ -2430,7 +2429,7 @@
           inverse ((- 1) ^ n * fact n :: 'a)"
     by (intro tendsto_intros rGamma_zeros) simp_all
   also have "inverse ((- 1) ^ n * fact n) = ?c"
-    by (simp_all add: field_simps reorient: power_mult_distrib)
+    by (simp_all add: field_simps flip: power_mult_distrib)
   finally show "(\<lambda>z. inverse (rGamma z / (z + of_nat n))) \<midarrow> (- of_nat n) \<rightarrow> ?c" .
 qed