--- 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; *)