diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Fixedpt.thy
--- a/src/ZF/Fixedpt.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Fixedpt.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
 
 Fixedpt = ZF + "domrange" +
 consts
-  bnd_mono    :: "[i,i=>i]=>o"
-  lfp, gfp    :: "[i,i=>i]=>i"
+  bnd_mono    :: [i,i=>i]=>o
+  lfp, gfp    :: [i,i=>i]=>i
 
 defs
   (*monotone operator from Pow(D) to itself*)