diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Sat Apr 11 11:56:40 2015 +0100
@@ -624,7 +624,7 @@
       by blast
   }
   then show ?thesis
-    unfolding LIMSEQ_def by blast
+    unfolding lim_sequentially by blast
 qed