# HG changeset patch
# User wenzelm
# Date 1146430201 -7200
# Node ID 351e1b1ea2514cfb282150bf177e8a19a45a613b
# Parent  d5236f5b0a7110be291dfd6e755d95b0ec23a479
AxClass.define_class_i;

diff -r d5236f5b0a71 -r 351e1b1ea251 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sun Apr 30 22:49:59 2006 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sun Apr 30 22:50:01 2006 +0200
@@ -205,7 +205,7 @@
                        (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
                         HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
       in
-          AxClass.add_axclass_i (cl_name, ["HOL.type"]) []
+          AxClass.define_class_i (cl_name, ["HOL.type"]) []
                 [((cl_name ^ "1", [Simplifier.simp_add]), [axiom1]),
                  ((cl_name ^ "2", []), [axiom2]),                           
                  ((cl_name ^ "3", []), [axiom3])] thy                          
@@ -254,7 +254,7 @@
           val axiom1   = HOLogic.mk_Trueprop (HOLogic.mk_mem (csupp $ x, cfinites));
 
        in  
-        AxClass.add_axclass_i (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy            
+        AxClass.define_class_i (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy            
        end) ak_names_types thy8; 
 
      (* proves that every fs_<ak>-type together with <ak>-type   *)
@@ -303,7 +303,7 @@
 			   (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
                                            cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
 	       in  
-		 AxClass.add_axclass_i (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy'  
+		 AxClass.define_class_i (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy'  
 	       end) ak_names_types thy) ak_names_types thy12;
 
         (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem;     *)