--- a/src/HOL/Multivariate_Analysis/Gamma.thy Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy Wed Feb 24 15:51:01 2016 +0000
@@ -1738,7 +1738,7 @@
moreover from z double_in_nonpos_Ints_imp[of z] have "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto
hence "?g \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
- using lim_subseq[of "op * 2", OF _ Gamma_series'_LIMSEQ, of "2*z"]
+ using LIMSEQ_subseq_LIMSEQ[OF Gamma_series'_LIMSEQ, of "op*2" "2*z"]
by (intro tendsto_intros Gamma_series'_LIMSEQ)
(simp_all add: o_def subseq_def Gamma_eq_zero_iff)
ultimately have "?h \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"