src/HOL/Hyperreal/Filter.thy

   assumes infinite: "A \<in> F \<Longrightarrow> infinite A"
 
 lemma (in freeultrafilter) finite: "finite A \<Longrightarrow> A \<notin> F"
 by (erule contrapos_pn, erule infinite)
 
-lemma (in freeultrafilter) filter: "filter F" .
+lemma (in freeultrafilter) filter: "filter F" by intro_locales
 
 lemma (in freeultrafilter) ultrafilter: "ultrafilter F"
-by (rule ultrafilter.intro)
+  by intro_locales
+
 
 subsection {* Collect properties *}
 
 lemma (in filter) Collect_ex:
   "({n. \<exists>x. P n x} \<in> F) = (\<exists>X. {n. P n (X n)} \<in> F)"

   proof (rule freeultrafilter_axioms.intro)
     fix A assume "A \<in> U"
     with U show "infinite A" by (rule mem_superfrechet_all_infinite)
   qed
   from fil ultra free have "freeultrafilter U"
-    by (rule freeultrafilter.intro)
+    by (rule freeultrafilter.intro [OF ultrafilter.intro])
+    (* FIXME: intro_locales should use chained facts *)
   thus ?thesis ..
 qed
 
 lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex