src/ZF/ex/Term.thy

--- a/src/ZF/ex/Term.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Term.thy	Mon May 21 14:36:24 2001 +0200
@@ -12,7 +12,7 @@
   term      :: i=>i
 
 datatype
-  "term(A)" = Apply ("a: A", "l: list(term(A))")
+  "term(A)" = Apply ("a \\<in> A", "l \\<in> list(term(A))")
   monos        list_mono
 
   type_elims  "[make_elim (list_univ RS subsetD)]"