src/HOL/Library/Formal_Power_Series.thy

--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -11,7 +11,7 @@
 
 subsection {* The type of formal power series*}
 
-typedef (open) 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
+typedef 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
   morphisms fps_nth Abs_fps
   by simp