src/ZF/Sum.thy

--- a/src/ZF/Sum.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Sum.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,10 +9,10 @@
 
 Sum = Bool + "simpdata" +
 consts
-    "+"    	:: "[i,i]=>i"      		(infixr 65)
-    Inl,Inr     :: "i=>i"
-    case        :: "[i=>i, i=>i, i]=>i"
-    Part        :: "[i,i=>i] => i"
+    "+"    	:: [i,i]=>i      		(infixr 65)
+    Inl,Inr     :: i=>i
+    case        :: [i=>i, i=>i, i]=>i
+    Part        :: [i,i=>i] => i
 
 defs
     sum_def     "A+B == {0}*A Un {1}*B"