src/HOL/HOL.thy
changeset 25494 b2484a7912ac
parent 25460 b80087af2274
child 25534 d0b74fdd6067
     1.1 --- a/src/HOL/HOL.thy	Wed Nov 28 16:26:53 2007 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Nov 28 16:44:18 2007 +0100
     1.3 @@ -37,11 +37,7 @@
     1.4  
     1.5  classes type
     1.6  defaultsort type
     1.7 -
     1.8 -setup {*
     1.9 -  Typedecl.interpretation (fn a => fn thy => AxClass.axiomatize_arity
    1.10 -    (a, replicate (Sign.arity_number thy a) @{sort type}, @{sort type}) thy)
    1.11 -*}
    1.12 +setup {* ObjectLogic.add_base_sort @{sort type} *}
    1.13  
    1.14  arities
    1.15    "fun" :: (type, type) type