src/ZF/ex/Term.thy

--- a/src/ZF/ex/Term.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Term.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -28,8 +28,8 @@
 
 defs
   term_rec_def
-   "term_rec(t,d) == \
-\   Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
+   "term_rec(t,d) == 
+   Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
 
   term_map_def	"term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"