# HG changeset patch
# User wenzelm
# Date 1196264658 -3600
# Node ID b2484a7912ac2190736e31f8c0c7116620f78c85
# Parent  50d566776a26ac9c3bb5bcdab6dffcc5193fd153
replaced typedecl interpretation by ObjectLogic.typedecl (based on base_sort);

diff -r 50d566776a26 -r b2484a7912ac 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