diff -r f061d2435d63 -r 5e407f2a3323 src/HOL/Hoare/Arith2.thy
--- a/src/HOL/Hoare/Arith2.thy	Wed Nov 29 16:58:30 1995 +0100
+++ b/src/HOL/Hoare/Arith2.thy	Wed Nov 29 17:01:41 1995 +0100
@@ -9,12 +9,12 @@
 Arith2 = Arith +
 
 consts
-  divides :: "[nat, nat] => bool"			(infixl 70)
-  cd	  :: "[nat, nat, nat] => bool"
-  gcd	  :: "[nat, nat] => nat"
+  divides :: [nat, nat] => bool			(infixl 70)
+  cd	  :: [nat, nat, nat] => bool
+  gcd	  :: [nat, nat] => nat
 
-  pow	  :: "[nat, nat] => nat"			(infixl 75)
-  fac	  :: "nat => nat"
+  pow	  :: [nat, nat] => nat			(infixl 75)
+  fac	  :: nat => nat
 
 defs
   divides_def	"x divides n == 0<n & 0<x & (n mod x) = 0"