diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -287,7 +287,7 @@
             by (simp only: numerals even_nat_div_two_times_two [OF `even w`])
           have "Ipol ls P * Ipol ls P = Ipol ls P ^ Suc (Suc 0)"
             by simp
-          then have "Ipol ls P * Ipol ls P = Ipol ls P ^ 2"
+          then have "Ipol ls P * Ipol ls P = (Ipol ls P)\<^sup>2"
             by (simp add: numerals)
           with Suc show ?thesis
             by (auto simp add: power_mult [symmetric, of _ 2 _] two_times mul_ci sqr_ci