1.1 --- a/src/HOL/HOL.thy	Fri Nov 23 21:09:32 2007 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Nov 23 21:09:33 2007 +0100
     1.3 @@ -38,16 +38,19 @@
     1.4  classes type
     1.5  defaultsort type
     1.6  
     1.7 +setup {*
     1.8 +  Typedecl.interpretation (fn a => fn thy => AxClass.axiomatize_arity
     1.9 +    (a, replicate (Sign.arity_number thy a) @{sort type}, @{sort type}) thy)
    1.10 +*}
    1.11 +
    1.12 +arities
    1.13 +  "fun" :: (type, type) type
    1.14 +  itself :: (type) type
    1.15 +
    1.16  global
    1.17  
    1.18  typedecl bool
    1.19  
    1.20 -arities
    1.21 -  bool :: type
    1.22 -  "fun" :: (type, type) type
    1.23 -
    1.24 -  itself :: (type) type
    1.25 -
    1.26  judgment
    1.27    Trueprop      :: "bool => prop"                   ("(_)" 5)
    1.28