diff -r d92cfed6c6b2 -r 1ba61c7b129f src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Sun Jun 07 19:38:32 2009 -0700
+++ b/src/HOL/RealVector.thy	Sun Jun 07 20:57:24 2009 -0700
@@ -419,7 +419,7 @@
 subsection {* Topological spaces *}
 
 class "open" =
-  fixes "open" :: "'a set set"
+  fixes "open" :: "'a set \<Rightarrow> bool"
 
 class topological_space = "open" +
   assumes open_UNIV [simp, intro]: "open UNIV"