diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/SetInterval.thy	Tue Sep 07 10:05:19 2010 +0200
@@ -241,7 +241,7 @@
 lemma atLeastatMost_psubset_iff:
   "{a..b} < {c..d} \<longleftrightarrow>
    ((~ a <= b) | c <= a & b <= d & (c < a | b < d))  &  c <= d"
-by(simp add: psubset_eq expand_set_eq less_le_not_le)(blast intro: order_trans)
+by(simp add: psubset_eq set_ext_iff less_le_not_le)(blast intro: order_trans)
 
 lemma atLeastAtMost_singleton_iff[simp]:
   "{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"