diff -r 42e9fd3ec1a3 -r 74909ecaf20a src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Thu Dec 14 22:08:35 2006 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Dec 14 22:09:26 2006 +0100
@@ -102,7 +102,7 @@
 
 text{*Also, proof of various properties of @{term FreeUltrafilterNat}: 
 an arbitrary free ultrafilter*}
-
+(*
 lemma FreeUltrafilterNat_Ex: "\<exists>U::nat set set. freeultrafilter U"
 by (rule nat_infinite [THEN freeultrafilter_Ex])
 
@@ -190,11 +190,12 @@
 
 
 text{*One further property of our free ultrafilter*}
+
 lemma FreeUltrafilterNat_Un:
      "X Un Y \<in> FreeUltrafilterNat  
       ==> X \<in> FreeUltrafilterNat | Y \<in> FreeUltrafilterNat"
 by (auto, ultra)
-
+*)
 
 subsection{*Properties of @{term starrel}*}
 
@@ -301,7 +302,7 @@
 apply (simp add: omega_def)
 apply (simp add: star_of_def star_n_eq_iff)
 apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] 
-            lemma_finite_omega_set [THEN FreeUltrafilterNat_finite])
+            lemma_finite_omega_set [THEN FreeUltrafilterNat.finite])
 done
 
 lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> omega"
@@ -320,7 +321,7 @@
 
 lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\<exists>x. hypreal_of_real x = epsilon)"
 by (auto simp add: epsilon_def star_of_def star_n_eq_iff
-                   lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite])
+                   lemma_finite_epsilon_set [THEN FreeUltrafilterNat.finite])
 
 lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> epsilon"
 by (insert not_ex_hypreal_of_real_eq_epsilon, auto)