src/HOL/Nominal/nominal_atoms.ML
changeset 19509 351e1b1ea251
parent 19494 2e909d5309f4
child 19548 c0a896828194
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sun Apr 30 22:49:59 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sun Apr 30 22:50:01 2006 +0200
     1.3 @@ -205,7 +205,7 @@
     1.4                         (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
     1.5                          HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
     1.6        in
     1.7 -          AxClass.add_axclass_i (cl_name, ["HOL.type"]) []
     1.8 +          AxClass.define_class_i (cl_name, ["HOL.type"]) []
     1.9                  [((cl_name ^ "1", [Simplifier.simp_add]), [axiom1]),
    1.10                   ((cl_name ^ "2", []), [axiom2]),                           
    1.11                   ((cl_name ^ "3", []), [axiom3])] thy                          
    1.12 @@ -254,7 +254,7 @@
    1.13            val axiom1   = HOLogic.mk_Trueprop (HOLogic.mk_mem (csupp $ x, cfinites));
    1.14  
    1.15         in  
    1.16 -        AxClass.add_axclass_i (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy            
    1.17 +        AxClass.define_class_i (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy            
    1.18         end) ak_names_types thy8; 
    1.19  
    1.20       (* proves that every fs_<ak>-type together with <ak>-type   *)
    1.21 @@ -303,7 +303,7 @@
    1.22  			   (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
    1.23                                             cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
    1.24  	       in  
    1.25 -		 AxClass.add_axclass_i (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy'  
    1.26 +		 AxClass.define_class_i (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy'  
    1.27  	       end) ak_names_types thy) ak_names_types thy12;
    1.28  
    1.29          (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem;     *)