diff -r 75e163863e16 -r 8ce8c4d13d4d src/ZF/arith.thy
--- a/src/ZF/arith.thy	Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/arith.thy	Fri Sep 17 16:16:38 1993 +0200
@@ -16,7 +16,7 @@
     "#-" :: "[i,i]=>i"      		(infixl 65)
 
 rules
-    rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(n, a, %m. b(m, f`m)))"
+    rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
 
     add_def  "m#+n == rec(m, n, %u v.succ(v))"
     diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))"