diff -r e1309df633c6 -r 2c227493ea56 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/RealVector.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -259,7 +259,7 @@
 by (simp add: divide_inverse)
 
 lemma of_real_power [simp]:
-  "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1,recpower}) ^ n"
+  "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1}) ^ n"
 by (induct n) simp_all
 
 lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
@@ -389,7 +389,7 @@
 done
 
 lemma Reals_power [simp]:
-  fixes a :: "'a::{real_algebra_1,recpower}"
+  fixes a :: "'a::{real_algebra_1}"
   shows "a \<in> Reals \<Longrightarrow> a ^ n \<in> Reals"
 apply (auto simp add: Reals_def)
 apply (rule range_eqI)
@@ -613,7 +613,7 @@
 by (simp add: divide_inverse norm_mult norm_inverse)
 
 lemma norm_power_ineq:
-  fixes x :: "'a::{real_normed_algebra_1,recpower}"
+  fixes x :: "'a::{real_normed_algebra_1}"
   shows "norm (x ^ n) \<le> norm x ^ n"
 proof (induct n)
   case 0 show "norm (x ^ 0) \<le> norm x ^ 0" by simp
@@ -628,7 +628,7 @@
 qed
 
 lemma norm_power:
-  fixes x :: "'a::{real_normed_div_algebra,recpower}"
+  fixes x :: "'a::{real_normed_div_algebra}"
   shows "norm (x ^ n) = norm x ^ n"
 by (induct n) (simp_all add: norm_mult)