--- a/src/HOL/Library/Polynomial_Factorial.thy Wed Sep 28 17:02:06 2016 +0100
+++ b/src/HOL/Library/Polynomial_Factorial.thy Thu Sep 29 11:24:36 2016 +0100
@@ -223,7 +223,7 @@
subsection \<open>Mapping polynomials\<close>
definition map_poly
- :: "('a :: comm_semiring_0 \<Rightarrow> 'b :: comm_semiring_0) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where
+ :: "('a :: zero \<Rightarrow> 'b :: zero) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where
"map_poly f p = Poly (map f (coeffs p))"
lemma map_poly_0 [simp]: "map_poly f 0 = 0"