# HG changeset patch
# User haftmann
# Date 1195848573 -3600
# Node ID b80087af22743a4d54fd1ad4da9f3fecd1b45c89
# Parent  d1dce7d0731c4caa1b6ecce84d8ace0b623ee5bd
interpretation of typedecls: instantiation to class type

diff -r d1dce7d0731c -r b80087af2274 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Nov 23 21:09:32 2007 +0100
+++ b/src/HOL/HOL.thy	Fri Nov 23 21:09:33 2007 +0100
@@ -38,16 +38,19 @@
 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)
+*}
+
+arities
+  "fun" :: (type, type) type
+  itself :: (type) type
+
 global
 
 typedecl bool
 
-arities
-  bool :: type
-  "fun" :: (type, type) type
-
-  itself :: (type) type
-
 judgment
   Trueprop      :: "bool => prop"                   ("(_)" 5)
 
diff -r d1dce7d0731c -r b80087af2274 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Nov 23 21:09:32 2007 +0100
+++ b/src/HOL/Set.thy	Fri Nov 23 21:09:33 2007 +0100
@@ -17,7 +17,6 @@
 global
 
 typedecl 'a set
-arities set :: (type) type
 
 consts
   "{}"          :: "'a set"                             ("{}")