--- a/src/HOL/HOL.thy Mon Feb 10 21:00:56 2014 +0100
+++ b/src/HOL/HOL.thy Mon Feb 10 21:03:28 2014 +0100
@@ -49,9 +49,11 @@
default_sort type
setup {* Object_Logic.add_base_sort @{sort type} *}
-arities
- "fun" :: (type, type) type
- itself :: (type) type
+axiomatization where fun_arity: "OFCLASS('a \<Rightarrow> 'b, type_class)"
+instance "fun" :: (type, type) type by (rule fun_arity)
+
+axiomatization where itself_arity: "OFCLASS('a itself, type_class)"
+instance itself :: (type) type by (rule itself_arity)
typedecl bool