--- a/src/ZF/ex/Term.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/Term.thy Tue Nov 29 00:31:31 1994 +0100
@@ -26,7 +26,7 @@
type_intrs "[list_univ RS subsetD]"
*)
-rules
+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))"