src/ZF/OrderArith.thy

--- a/src/ZF/OrderArith.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/OrderArith.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
 
 OrderArith = Order + Sum + 
 consts
-  radd, rmult      :: "[i,i,i,i]=>i"
-  rvimage          :: "[i,i,i]=>i"
+  radd, rmult      :: [i,i,i,i]=>i
+  rvimage          :: [i,i,i]=>i
 
 defs
   (*disjoint sum of two relations; underlies ordinal addition*)