1.1 --- a/src/HOL/Library/Polynomial.thy	Wed Sep 23 09:50:38 2015 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Sep 24 13:33:42 2015 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4  
     1.5  subsection \<open>Definition of type @{text poly}\<close>
     1.6  
     1.7 -typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
     1.8 +typedef (overloaded) 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
     1.9    morphisms coeff Abs_poly by (auto intro!: ALL_MOST)
    1.10  
    1.11  setup_lifting type_definition_poly