--- a/src/HOL/Real/PReal.thy Sun Dec 18 20:10:15 2005 +0100
+++ b/src/HOL/Real/PReal.thy Mon Dec 19 09:19:08 2005 +0100
@@ -139,8 +139,8 @@
subsection{*@{term preal_of_prat}: the Injection from prat to preal*}
lemma rat_less_set_mem_preal: "0 < y ==> {u::rat. 0 < u & u < y} \<in> preal"
-apply (auto simp del: empty_Collect_eq simp add: preal_def cut_def intro: order_less_trans)
-apply (force simp only: eq_commute [of "{}"] interval_empty_iff)
+apply (auto simp add: preal_def cut_def intro: order_less_trans)
+apply (blast dest:dense)
apply (blast dest: dense intro: order_less_trans)
done