src/HOL/Computational_Algebra/Formal_Power_Series.thy

--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -1425,6 +1425,8 @@
 
 end
 
+instance fps :: (field) normalization_euclidean_semiring ..
+
 instantiation fps :: (field) euclidean_ring_gcd
 begin
 definition fps_gcd_def: "(gcd :: 'a fps \<Rightarrow> _) = Euclidean_Algorithm.gcd"