diff -r 5f690b184f91 -r 24eef3860714 src/HOL/Arith.thy
--- a/src/HOL/Arith.thy	Fri Mar 17 22:46:26 1995 +0100
+++ b/src/HOL/Arith.thy	Mon Mar 20 15:35:28 1995 +0100
@@ -20,8 +20,8 @@
   add_def   "m+n == nat_rec m n (%u v. Suc(v))"
   diff_def  "m-n == nat_rec n m (%u v. pred(v))"
   mult_def  "m*n == nat_rec m 0 (%u v. n + v)"
-  mod_def   "m mod n == wfrec (trancl pred_nat) m (%j f.(if (j<n) j (f (j-n))))"
-  div_def   "m div n == wfrec (trancl pred_nat) m (%j f.(if (j<n) 0 (Suc (f (j-n)))))"
+  mod_def   "m mod n == wfrec (trancl pred_nat) m (%j f.if j<n then j else f (j-n))"
+  div_def   "m div n == wfrec (trancl pred_nat) m (%j f.if j<n then 0 else Suc (f (j-n)))"
 end
 
 (*"Difference" is subtraction of natural numbers.