src/HOL/UNITY/Comp/Alloc.thy

   apply (unfold system_safety_def)
   apply (tactic \<open>resolve_tac @{context} [Always_Int_rule [@{thm System_sum_bounded},
     @{thm Always_tokens_giv_le_allocGiv}, @{thm Always_tokens_allocRel_le_rel}] RS
     @{thm Always_weaken}] 1\<close>)
   apply auto
-  apply (rule setsum_fun_mono [THEN order_trans])
+  apply (rule sum_fun_mono [THEN order_trans])
   apply (drule_tac [2] order_trans)
-  apply (rule_tac [2] add_le_mono [OF order_refl setsum_fun_mono])
+  apply (rule_tac [2] add_le_mono [OF order_refl sum_fun_mono])
   prefer 3 apply assumption
   apply auto
   done
 
 subsection \<open>Proof of the progress property (2)\<close>