diff -r 2e9a86203d59 -r 934a58983311 Sum.thy
--- a/Sum.thy	Thu Mar 17 14:08:08 1994 +0100
+++ b/Sum.thy	Thu Mar 17 17:02:49 1994 +0100
@@ -7,17 +7,23 @@
 *)
 
 Sum = Prod +
-types   "+" 2      (infixl 10)
-arities "+"     :: (term,term)term
+
+types
+  ('a,'b) "+"		      (infixl 10)
+
+arities
+  "+"      :: (term,term)term
+
 consts
-   Inl_Rep	:: "['a,'a,'b,bool] => bool"
-   Inr_Rep	:: "['b,'a,'b,bool] => bool"
-   Sum		:: "(['a,'b,bool] => bool)set"
-   Rep_Sum	:: "'a + 'b => (['a,'b,bool] => bool)"
-   Abs_Sum	:: "(['a,'b,bool] => bool) => 'a+'b"
-   Inl		:: "'a => 'a+'b"
-   Inr		:: "'b => 'a+'b"
-   sum_case	:: "['a+'b, 'a=>'c,'b=>'c] =>'c"
+  Inl_Rep  :: "['a,'a,'b,bool] => bool"
+  Inr_Rep  :: "['b,'a,'b,bool] => bool"
+  Sum      :: "(['a,'b,bool] => bool)set"
+  Rep_Sum  :: "'a + 'b => (['a,'b,bool] => bool)"
+  Abs_Sum  :: "(['a,'b,bool] => bool) => 'a+'b"
+  Inl	   :: "'a => 'a+'b"
+  Inr	   :: "'b => 'a+'b"
+  sum_case :: "['a+'b, 'a=>'c,'b=>'c] =>'c"
+
 rules
   Inl_Rep_def	"Inl_Rep == (%a. %x y p. x=a & p)"
   Inr_Rep_def	"Inr_Rep == (%b. %x y p. y=b & ~p)"