# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1475144676 -3600
# Node ID fb03766658f41b2b554623d0e38ac23ea3d5fa04
# Parent  b5d7806c9396169f61965d768861afdd3bfaa6f7
Generalised the type of map_poly

diff -r b5d7806c9396 -r fb03766658f4 src/HOL/Library/Polynomial_Factorial.thy
--- 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"