# HG changeset patch
# User huffman
# Date 1244433444 25200
# Node ID 1ba61c7b129f3175c9aa9071e7a28890ab3bd14c
# Parent  d92cfed6c6b201d5181ce367dfc5238d19f89dd8
fix type of open

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"