diff -r 32b888e1a170 -r 504d72a39638 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Wed Jun 01 11:51:25 2011 +0200
+++ b/src/HOL/Wellfounded.thy	Wed Jun 01 15:53:47 2011 +0200
@@ -864,7 +864,7 @@
 
 lemma wf_bounded_measure:
 fixes ub :: "'a \<Rightarrow> nat" and f :: "'a \<Rightarrow> nat"
-assumes "!!a b. (b,a) : r \<Longrightarrow> ub b \<le> ub a & ub a > f b & f b > f a"
+assumes "!!a b. (b,a) : r \<Longrightarrow> ub b \<le> ub a & ub a \<ge> f b & f b > f a"
 shows "wf r"
 apply(rule wf_subset[OF wf_measure[of "%a. ub a - f a"]])
 apply (auto dest: assms)
@@ -873,11 +873,11 @@
 lemma wf_bounded_set:
 fixes ub :: "'a \<Rightarrow> 'b set" and f :: "'a \<Rightarrow> 'b set"
 assumes "!!a b. (b,a) : r \<Longrightarrow>
-  finite(ub a) & ub b \<subseteq> ub a & ub a \<supset> f b & f b \<supset> f a"
+  finite(ub a) & ub b \<subseteq> ub a & ub a \<supseteq> f b & f b \<supset> f a"
 shows "wf r"
 apply(rule wf_bounded_measure[of r "%a. card(ub a)" "%a. card(f a)"])
 apply(drule assms)
-apply (blast intro: card_mono finite_subset  psubset_card_mono dest: psubset_eq[THEN iffD2])
+apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2])
 done