--- a/src/HOL/IMP/Abs_Int0.thy Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Wed Aug 19 19:18:19 2015 +0100
@@ -317,7 +317,7 @@
"m_s S X = (\<Sum> x \<in> X. m(S x))"
lemma m_s_h: "finite X \<Longrightarrow> m_s S X \<le> h * card X"
-by(simp add: m_s_def) (metis mult.commute of_nat_id setsum_bounded[OF h])
+by(simp add: m_s_def) (metis mult.commute of_nat_id setsum_bounded_above[OF h])
fun m_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^sub>o") where
"m_o (Some S) X = m_s S X" |