diff -r 6f2986464280 -r 40e5c97e988d src/HOL/Arith.thy
--- a/src/HOL/Arith.thy	Thu Dec 04 09:05:59 1997 +0100
+++ b/src/HOL/Arith.thy	Thu Dec 04 12:44:37 1997 +0100
@@ -11,13 +11,8 @@
 instance
   nat :: {plus, minus, times, power}
 
-consts
-  pred      :: nat => nat
-  (* size of a datatype value; overloaded *)
-  size      :: 'a => nat
-
-defs
-  pred_def  "pred(m) == case m of 0 => 0 | Suc n => n"
+(* size of a datatype value; overloaded *)
+consts size :: 'a => nat
 
 primrec "op +" nat 
   add_0    "0 + n = n"
@@ -25,7 +20,10 @@
 
 primrec "op -" nat 
   diff_0   "m - 0 = m"
-  diff_Suc "m - Suc n = pred(m - n)"
+  diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
+
+syntax pred :: nat => nat
+translations "pred m" => "m - 1"
 
 primrec "op *"  nat 
   mult_0   "0 * n = 0"