src/ZF/Nat.thy

--- a/src/ZF/Nat.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Nat.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,9 +8,9 @@
 
 Nat = Ordinal + Bool + "mono" +
 consts
-    nat 	::      "i"
-    nat_case    ::      "[i, i=>i, i]=>i"
-    nat_rec     ::      "[i, i, [i,i]=>i]=>i"
+    nat 	::      i
+    nat_case    ::      [i, i=>i, i]=>i
+    nat_rec     ::      [i, i, [i,i]=>i]=>i
 
 defs