Deleted instance "set :: (type) power" and moved instance
"fun :: (type, type) power" to the beginning of the theory

--- a/src/HOL/Relation_Power.thy	Wed May 07 10:56:40 2008 +0200
+++ b/src/HOL/Relation_Power.thy	Wed May 07 10:56:41 2008 +0200
@@ -11,8 +11,8 @@
 begin
 
 instance
-  set :: (type) power ..
-      --{* only type @{typ "('a * 'a) set"} should be in class @{text power}!*}
+  "fun" :: (type, type) power ..
+      --{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
 
 overloading
   relpow \<equiv> "power \<Colon> ('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a \<times> 'a) set"  (unchecked)
@@ -26,10 +26,6 @@
 
 end
 
-instance
-  "fun" :: (type, type) power ..
-      --{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
-
 overloading
   funpow \<equiv> "power \<Colon>  ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" (unchecked)
 begin