src/HOL/NSA/Filter.thy

 qed
 
 subsection {* Ultrafilter Theorem *}
 
 text "A locale makes proof of ultrafilter Theorem more modular"
-locale (open) UFT =
+locale UFT =
   fixes   frechet :: "'a set set"
   and     superfrechet :: "'a set set set"
 
   assumes infinite_UNIV: "infinite (UNIV :: 'a set)"
 

       by (rule freeultrafilter.intro [OF ultrafilter.intro])
       (* FIXME: unfold_locales should use chained facts *)
   qed
 qed
 
-lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex
+lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex [OF UFT.intro]
 
 hide (open) const filter
 
 end