src/HOL/NSA/Filter.thy
changeset 36176 3fe7e97ccca8
parent 28823 dcbef866c9e2
child 41589 bbd861837ebc
--- 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