diff -r 05e57f1879ee -r 75a9ef36b1fe src/HOL/Arith.thy
--- a/src/HOL/Arith.thy	Mon Mar 09 16:17:28 1998 +0100
+++ b/src/HOL/Arith.thy	Mon Mar 09 16:30:55 1998 +0100
@@ -22,9 +22,6 @@
   diff_0   "m - 0 = m"
   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"
   mult_Suc "Suc m * n = n + (m * n)"