src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Wed Nov 28 16:26:53 2007 +0100
+++ b/src/HOL/HOL.thy	Wed Nov 28 16:44:18 2007 +0100
@@ -37,11 +37,7 @@
 
 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)
-*}
+setup {* ObjectLogic.add_base_sort @{sort type} *}
 
 arities
   "fun" :: (type, type) type