diff -r 458e55fd0a33 -r fec1a04b7220 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy	Wed Apr 22 19:09:21 2009 +0200
@@ -253,12 +253,7 @@
   "vector_power x 0 = 1"
   | "vector_power x (Suc n) = x * vector_power x n"
 
-instantiation "^" :: (recpower,type) recpower
-begin
-  definition vec_power_def: "op ^ \<equiv> vector_power"
-  instance
-  apply (intro_classes) by (simp_all add: vec_power_def)
-end
+instance "^" :: (recpower,type) recpower ..
 
 instance "^" :: (semiring,type) semiring
   apply (intro_classes) by (vector ring_simps)+