src/HOL/Series.thy

--- a/src/HOL/Series.thy	Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/Series.thy	Wed May 25 11:49:40 2016 +0200
@@ -362,7 +362,7 @@
 
 end
 
-context --\<open>Separate contexts are necessary to allow general use of the results above, here.\<close>
+context \<comment>\<open>Separate contexts are necessary to allow general use of the results above, here.\<close>
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
 begin