--- a/src/HOL/Power.thy Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/Power.thy Wed Jan 21 23:40:23 2009 +0100
@@ -11,7 +11,7 @@
imports Nat
begin
-class power = type +
+class power =
fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80)
subsection{*Powers for Arbitrary Monoids*}