diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Arith.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,12 +8,12 @@
 
 Arith = Epsilon + "simpdata" +
 consts
-    rec  :: "[i, i, [i,i]=>i]=>i"
-    "#*" :: "[i,i]=>i"      		(infixl 70)
-    div  :: "[i,i]=>i"      		(infixl 70) 
-    mod  :: "[i,i]=>i"      		(infixl 70)
-    "#+" :: "[i,i]=>i"      		(infixl 65)
-    "#-" :: "[i,i]=>i"      		(infixl 65)
+    rec  :: [i, i, [i,i]=>i]=>i
+    "#*" :: [i,i]=>i      		(infixl 70)
+    div  :: [i,i]=>i      		(infixl 70) 
+    mod  :: [i,i]=>i      		(infixl 70)
+    "#+" :: [i,i]=>i      		(infixl 65)
+    "#-" :: [i,i]=>i      		(infixl 65)
 
 defs
     rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"