
diff -r 6af79184bef3 -r c184ec919c70 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri Jul 08 23:43:11 2016 +0200
+++ b/src/HOL/Transcendental.thy	Sat Jul 09 13:26:16 2016 +0200
@@ -36,7 +36,7 @@
   by (metis of_nat_fact of_real_of_nat_eq)
 
 lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)"
-  by (simp add: pochhammer_def)
+  by (simp add: pochhammer_setprod)
 
 lemma norm_fact [simp]:
   "norm (fact n :: 'a :: {real_normed_algebra_1}) = fact n"




