# HG changeset patch
# User wenzelm
# Date 1392062608 -3600
# Node ID a416780523e2369e13c6a9211a3143990964d451
# Parent  9218fa411c155a03d37ed218df59177713de03c1
more explicit axiomatization;

diff -r 9218fa411c15 -r a416780523e2 src/HOL/HOL.thy
--- 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