diff -r 7247cb62406c -r 1d43f86f48be src/HOL/UNITY/Comp/AllocImpl.thy
--- a/src/HOL/UNITY/Comp/AllocImpl.thy	Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Mon Dec 28 19:23:15 2015 +0100
@@ -375,7 +375,7 @@
 
 lemma alloc_refinement_lemma:
      "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s})
-      \<subseteq> {s. (SUM x: lessThan n. f x) \<le> (SUM x: lessThan n. g x s)}"
+      \<subseteq> {s. (\<Sum>x \<in> lessThan n. f x) \<le> (\<Sum>x \<in> lessThan n. g x s)}"
 apply (induct_tac "n")
 apply (auto simp add: lessThan_Suc)
 done