--- a/src/HOL/NatDef.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/NatDef.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -12,13 +12,8 @@
 
 (** type ind **)
 
-global
-
-types
-  ind
-
-arities
-  ind :: term
+types ind
+arities ind :: type
 
 consts
   Zero_Rep      :: ind
@@ -43,6 +38,8 @@
   Zero_RepI "Zero_Rep : Nat'"
   Suc_RepI  "i : Nat' ==> Suc_Rep i : Nat'"
 
+global
+
 typedef (Nat)
   nat = "Nat'"   (Nat'.Zero_RepI)