--- a/src/HOL/Library/Disjoint_Sets.thy Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/Library/Disjoint_Sets.thy Thu Dec 10 13:38:40 2015 +0000
@@ -79,7 +79,7 @@
"(\<And>n. A n \<subseteq> A (Suc n)) \<Longrightarrow> disjoint_family (\<lambda>i. A (Suc i) - A i)"
using lift_Suc_mono_le[of A]
by (auto simp add: disjoint_family_on_def)
- (metis insert_absorb insert_subset le_SucE le_antisym not_leE less_imp_le)
+ (metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le)
lemma disjoint_family_on_disjoint_image:
"disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)"