diff -r 36489d77c484 -r a14831ac3023 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Thu Apr 03 23:51:52 2014 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Apr 04 17:58:25 2014 +0100
@@ -3635,7 +3635,7 @@
   done
 
 lemma fps_sin_even: "fps_sin (- c) = - fps_sin c"
-  by (auto simp add: fps_eq_iff fps_sin_def)
+  by (auto simp add: divide_minus_left fps_eq_iff fps_sin_def)
 
 lemma fps_cos_odd: "fps_cos (- c) = fps_cos c"
   by (auto simp add: fps_eq_iff fps_cos_def)