HOL/Sum.thy: generalized the type of Part

--- a/Sum.thy	Fri Aug 19 16:18:44 1994 +0200
+++ b/Sum.thy	Mon Aug 22 10:56:45 1994 +0200
@@ -26,7 +26,7 @@
 
   (*disjoint sum for sets; the operator + is overloaded with wrong type!*)
   "plus"   :: "['a set, 'b set] => ('a+'b)set"      	(infixr 65)
-  Part     :: "['a set, 'a=>'a] => 'a set"
+  Part     :: "['a set, 'b=>'a] => 'a set"
 
 translations
   "case p of Inl(x) => a | Inr(y) => b" == "sum_case(%x.a, %y.b, p)"