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