Replaced instance "set :: (plus) plus" by "fun :: (type, type) plus"

--- a/src/HOL/Real/HahnBanach/Subspace.thy	Wed May 07 10:59:35 2008 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Wed May 07 10:59:36 2008 +0200
@@ -216,7 +216,7 @@
   set of all sums of elements from @{text U} and @{text V}.
 *}
 
-instance set :: (plus) plus ..
+instance "fun" :: (type, type) plus ..
 
 defs (overloaded)
   sum_def: "U + V \<equiv> {u + v | u v. u \<in> U \<and> v \<in> V}"