src/HOL/Library/Polynomial.thy

--- a/src/HOL/Library/Polynomial.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Polynomial.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -13,7 +13,7 @@
 
 definition "Poly = {f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"
 
-typedef (open) 'a poly = "Poly :: (nat => 'a::zero) set"
+typedef 'a poly = "Poly :: (nat => 'a::zero) set"
   morphisms coeff Abs_poly
   unfolding Poly_def by auto