diff -r f3d4ff75d9f2 -r 3ac1c0c0016e src/ZF/arith.thy
--- a/src/ZF/arith.thy	Tue Oct 05 13:15:01 1993 +0100
+++ b/src/ZF/arith.thy	Tue Oct 05 15:21:29 1993 +0100
@@ -21,6 +21,6 @@
     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))"
     mult_def "m#*n == rec(m, 0, %u v. n #+ v)"
-    mod_def  "m mod n == transrec(m, %j f. if(j:n, j, f`(j#-n)))"
-    div_def  "m div n == transrec(m, %j f. if(j:n, 0, succ(f`(j#-n))))"
+    mod_def  "m mod n == transrec(m, %j f. if(j<n, j, f`(j#-n)))"
+    div_def  "m div n == transrec(m, %j f. if(j<n, 0, succ(f`(j#-n))))"
 end