diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Bool.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -10,14 +10,14 @@
 
 Bool = ZF + "simpdata" +
 consts
-    "1"		:: "i"     	   ("1")
-    "2"         :: "i"             ("2")
-    bool        :: "i"
-    cond        :: "[i,i,i]=>i"
-    not		:: "i=>i"
-    "and"       :: "[i,i]=>i"      (infixl 70)
-    or		:: "[i,i]=>i"      (infixl 65)
-    xor		:: "[i,i]=>i"      (infixl 65)
+    "1"		:: i     	   ("1")
+    "2"         :: i             ("2")
+    bool        :: i
+    cond        :: [i,i,i]=>i
+    not		:: i=>i
+    "and"       :: [i,i]=>i      (infixl 70)
+    or		:: [i,i]=>i      (infixl 65)
+    xor		:: [i,i]=>i      (infixl 65)
 
 translations
    "1"  == "succ(0)"