# HG changeset patch
# User berghofe
# Date 1210150776 -7200
# Node ID 05fd4be26c4d2fed0a6ce7f0313b2d99c712c300
# Parent  2909150bd6145c45af017bbac712cb77c4470600
Replaced instance "set :: (plus) plus" by "fun :: (type, type) plus"

diff -r 2909150bd614 -r 05fd4be26c4d src/HOL/Real/HahnBanach/Subspace.thy
--- 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}"