src/ZF/ex/Ntree.thy

--- a/src/ZF/ex/Ntree.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Ntree.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -11,9 +11,9 @@
 
 Ntree = InfDatatype +
 consts
-  ntree    :: "i=>i"
-  maptree  :: "i=>i"
-  maptree2 :: "[i,i] => i"
+  ntree    :: i=>i
+  maptree  :: i=>i
+  maptree2 :: [i,i] => i
 
 datatype
   "ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")