diff -r 458e55fd0a33 -r fec1a04b7220 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Complex.thy	Wed Apr 22 19:09:21 2009 +0200
@@ -159,19 +159,7 @@
 
 subsection {* Exponentiation *}
 
-instantiation complex :: recpower
-begin
-
-primrec power_complex where
-  "z ^ 0     = (1\<Colon>complex)"
-| "z ^ Suc n = (z\<Colon>complex) * z ^ n"
-
-instance proof
-qed simp_all
-
-declare power_complex.simps [simp del]
-
-end
+instance complex :: recpower ..
 
 
 subsection {* Numerals and Arithmetic *}