src/HOL/Library/Formal_Power_Series.thy

--- a/src/HOL/Library/Formal_Power_Series.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -218,7 +218,7 @@
 qed
 
 instance fps :: (zero_neq_one) zero_neq_one
-  by default (simp add: expand_fps_eq)
+  by standard (simp add: expand_fps_eq)
 
 instance fps :: (semiring_0) semiring
 proof