src/ZF/Epsilon.thy

--- a/src/ZF/Epsilon.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Epsilon.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
 
 Epsilon = Nat + "mono" +
 consts
-    eclose,rank ::      "i=>i"
-    transrec    ::      "[i, [i,i]=>i] =>i"
+    eclose,rank ::      i=>i
+    transrec    ::      [i, [i,i]=>i] =>i
 
 defs
   eclose_def	"eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"