--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Sep 02 14:27:55 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Sep 02 15:19:59 2011 -0700
@@ -914,7 +914,7 @@
lemma eventually_within_le: "eventually P (at a within S) \<longleftrightarrow>
(\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)" (is "?lhs = ?rhs")
unfolding eventually_within
-by auto (metis Rats_dense_in_nn_real order_le_less_trans order_refl)
+by auto (metis dense order_le_less_trans)
lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)"
unfolding trivial_limit_def