src/ZF/ex/Term.thy

--- a/src/ZF/ex/Term.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Term.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,13 +9,13 @@
 
 Term = List +
 consts
-  term_rec  :: "[i, [i,i,i]=>i] => i"
-  term_map  :: "[i=>i, i] => i"
-  term_size :: "i=>i"
-  reflect   :: "i=>i"
-  preorder  :: "i=>i"
+  term_rec  :: [i, [i,i,i]=>i] => i
+  term_map  :: [i=>i, i] => i
+  term_size :: i=>i
+  reflect   :: i=>i
+  preorder  :: i=>i
 
-  term      :: "i=>i"
+  term      :: i=>i
 
 datatype
   "term(A)" = Apply ("a: A", "l: list(term(A))")