--- 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