diff -r 857444b28267 -r a28879118978 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Mon Nov 21 10:44:14 2005 +0100
+++ b/src/HOL/Real/PReal.thy	Mon Nov 21 11:14:11 2005 +0100
@@ -24,7 +24,7 @@
 
 lemma interval_empty_iff:
      "({y::'a::ordered_field. x < y & y < z} = {}) = (~(x < z))"
-by (blast dest: dense intro: order_less_trans)
+by (auto dest: dense)
 
 
 constdefs