diff -r bb18eed53ed6 -r a1119cf551e8 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Aug 13 16:25:47 2013 +0200
@@ -3352,7 +3352,7 @@
 next
   case False obtain y where "y\<in>s" and y:"\<forall>x\<in>s. dist z y \<le> dist z x"
     using distance_attains_inf[OF assms(2) False] by auto
-  show ?thesis apply(rule_tac x="y - z" in exI, rule_tac x="inner (y - z) z + (norm(y - z))\<twosuperior> / 2" in exI)
+  show ?thesis apply(rule_tac x="y - z" in exI, rule_tac x="inner (y - z) z + (norm(y - z))\<^sup>2 / 2" in exI)
     apply rule defer apply rule proof-
     fix x assume "x\<in>s"
     have "\<not> 0 < inner (z - y) (x - y)" apply(rule_tac notI) proof(drule closer_point_lemma)
@@ -3363,7 +3363,7 @@
         using `x\<in>s` `y\<in>s` by (auto simp add: dist_commute algebra_simps) qed
     moreover have "0 < norm (y - z) ^ 2" using `y\<in>s` `z\<notin>s` by auto
     hence "0 < inner (y - z) (y - z)" unfolding power2_norm_eq_inner by simp
-    ultimately show "inner (y - z) z + (norm (y - z))\<twosuperior> / 2 < inner (y - z) x"
+    ultimately show "inner (y - z) z + (norm (y - z))\<^sup>2 / 2 < inner (y - z) x"
       unfolding power2_norm_eq_inner and not_less by (auto simp add: field_simps inner_commute inner_diff)
   qed(insert `y\<in>s` `z\<notin>s`, auto)
 qed