--- a/src/HOL/NSA/Filter.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/NSA/Filter.thy Fri Apr 16 21:28:09 2010 +0200
@@ -403,6 +403,6 @@
lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex [OF UFT.intro]
-hide (open) const filter
+hide_const (open) filter
end