src/HOL/Library/Extended_Real.thy

--- a/src/HOL/Library/Extended_Real.thy	Wed Sep 21 06:41:34 2011 -0700
+++ b/src/HOL/Library/Extended_Real.thy	Wed Sep 21 08:28:53 2011 -0700
@@ -765,14 +765,6 @@
 
 subsubsection {* Power *}
 
-instantiation ereal :: power
-begin
-primrec power_ereal where
-  "power_ereal x 0 = 1" |
-  "power_ereal x (Suc n) = x * x ^ n"
-instance ..
-end
-
 lemma ereal_power[simp]: "(ereal x) ^ n = ereal (x^n)"
   by (induct n) (auto simp: one_ereal_def)