diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/CardinalArith.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,12 +9,12 @@
 CardinalArith = Cardinal + OrderArith + Arith + Finite + 
 consts
 
-  InfCard       :: "i=>o"
-  "|*|"         :: "[i,i]=>i"       (infixl 70)
-  "|+|"         :: "[i,i]=>i"       (infixl 65)
-  csquare_rel   :: "i=>i"
-  jump_cardinal :: "i=>i"
-  csucc         :: "i=>i"
+  InfCard       :: i=>o
+  "|*|"         :: [i,i]=>i       (infixl 70)
+  "|+|"         :: [i,i]=>i       (infixl 65)
+  csquare_rel   :: i=>i
+  jump_cardinal :: i=>i
+  csucc         :: i=>i
 
 defs