--- a/src/HOL/Library/Convex.thy Thu Oct 31 16:54:22 2013 +0100
+++ b/src/HOL/Library/Convex.thy Fri Nov 01 18:51:14 2013 +0100
@@ -362,7 +362,7 @@
shows "convex {x - y| x y. x \<in> s \<and> y \<in> t}"
proof -
have "{x - y| x y. x \<in> s \<and> y \<in> t} = {x + y |x y. x \<in> s \<and> y \<in> uminus ` t}"
- unfolding diff_def by auto
+ by (auto simp add: diff_conv_add_uminus simp del: add_uminus_conv_diff)
then show ?thesis
using convex_sums[OF assms(1) convex_negations[OF assms(2)]] by auto
qed