src/ZF/Sum.thy

--- a/src/ZF/Sum.thy	Tue Jun 18 17:58:21 2002 +0200
+++ b/src/ZF/Sum.thy	Tue Jun 18 18:45:07 2002 +0200
@@ -12,10 +12,11 @@
 global
 
 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     :: "i=>i"
+    Inr     :: "i=>i"
+    "case"  :: "[i=>i, i=>i, i]=>i"
+    Part    :: "[i,i=>i] => i"
 
 local