src/HOL/Arith.thy

--- a/src/HOL/Arith.thy	Mon Nov 27 13:44:56 1995 +0100
+++ b/src/HOL/Arith.thy	Wed Nov 29 16:44:59 1995 +0100
@@ -12,8 +12,8 @@
   nat :: {plus, minus, times}
 
 consts
-  pred      :: "nat => nat"
-  div, mod  :: "[nat, nat] => nat"  (infixl 70)
+  pred      :: nat => nat
+  div, mod  :: [nat, nat] => nat  (infixl 70)
 
 defs
   pred_def  "pred(m) == nat_rec m 0 (%n r.n)"