interpretation of typedecls: instantiation to class type

--- a/src/HOL/HOL.thy	Fri Nov 23 21:09:32 2007 +0100
+++ b/src/HOL/HOL.thy	Fri Nov 23 21:09:33 2007 +0100
@@ -38,16 +38,19 @@
 classes type
 defaultsort type
 
+setup {*
+  Typedecl.interpretation (fn a => fn thy => AxClass.axiomatize_arity
+    (a, replicate (Sign.arity_number thy a) @{sort type}, @{sort type}) thy)
+*}
+
+arities
+  "fun" :: (type, type) type
+  itself :: (type) type
+
 global
 
 typedecl bool
 
-arities
-  bool :: type
-  "fun" :: (type, type) type
-
-  itself :: (type) type
-
 judgment
   Trueprop      :: "bool => prop"                   ("(_)" 5)
 

--- a/src/HOL/Set.thy	Fri Nov 23 21:09:32 2007 +0100
+++ b/src/HOL/Set.thy	Fri Nov 23 21:09:33 2007 +0100
@@ -17,7 +17,6 @@
 global
 
 typedecl 'a set
-arities set :: (type) type
 
 consts
   "{}"          :: "'a set"                             ("{}")