diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Library/Polynomial_FPS.thy
--- a/src/HOL/Library/Polynomial_FPS.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Library/Polynomial_FPS.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -67,7 +67,7 @@
 lemma fps_of_poly_sum_list: "fps_of_poly (sum_list xs) = sum_list (map fps_of_poly xs)"
   by (induction xs) (simp_all add: fps_of_poly_add)
   
-lemma fps_of_poly_setprod: "fps_of_poly (setprod f A) = setprod (\<lambda>x. fps_of_poly (f x)) A"
+lemma fps_of_poly_prod: "fps_of_poly (prod f A) = prod (\<lambda>x. fps_of_poly (f x)) A"
   by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_mult)
   
 lemma fps_of_poly_prod_list: "fps_of_poly (prod_list xs) = prod_list (map fps_of_poly xs)"
@@ -144,7 +144,7 @@
 lemmas fps_of_poly_simps =
   fps_of_poly_0 fps_of_poly_1 fps_of_poly_numeral fps_of_poly_const fps_of_poly_X
   fps_of_poly_add fps_of_poly_diff fps_of_poly_uminus fps_of_poly_mult fps_of_poly_smult
-  fps_of_poly_sum fps_of_poly_sum_list fps_of_poly_setprod fps_of_poly_prod_list
+  fps_of_poly_sum fps_of_poly_sum_list fps_of_poly_prod fps_of_poly_prod_list
   fps_of_poly_pCons fps_of_poly_pderiv fps_of_poly_power fps_of_poly_monom
   fps_of_poly_divide_numeral