# HG changeset patch
# User wenzelm
# Date 1146430212 -7200
# Node ID 5204c73a4d4625c92b6bcda18ec534b9265517c9
# Parent  73361110b570fcc9bb9c8f82d8205424f37e5268
AxClass.define_class_i, AxClass.get_definition;
Sign.primitive_arity;

diff -r 73361110b570 -r 5204c73a4d46 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Sun Apr 30 22:50:11 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Sun Apr 30 22:50:12 2006 +0200
@@ -343,8 +343,8 @@
 fun add_axclass_i (name, supsort) axs thy =
   let
     val (c, thy') = thy
-      |> AxClass.add_axclass_i (name, supsort) [] axs;
-    val {intro, axioms, ...} = AxClass.get_info thy' c;
+      |> AxClass.define_class_i (name, supsort) [] axs;
+    val {intro, axioms, ...} = AxClass.get_definition thy' c;
   in ((c, (intro, axioms)), thy') end;
 
 fun prove_interpretation_i (prfx, atts) expr insts tac thy =
@@ -535,7 +535,7 @@
       in () end;
     fun check_defs1 raw_defs c_req thy =
       let
-        val thy' = (Sign.add_arities_i [(tyco, asorts, sort)] o Theory.copy) thy
+        val thy' = (Sign.primitive_arity (tyco, asorts, sort) o Theory.copy) thy
       in (check_defs0 thy' raw_defs c_req; thy) end;
     fun mangle_alldef_name tyco sort =
       Thm.def_name ((space_implode "_" o map NameSpace.base) sort ^ "_" ^ NameSpace.base tyco);