Adapted to new interface of add_axclass_i.
authorberghofe
Thu Apr 27 17:48:17 2006 +0200 (2006-04-27)
changeset 194888bd2c840458e
parent 19487 d5e79a41bce0
child 19489 4441b637871b
Adapted to new interface of add_axclass_i.
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Thu Apr 27 17:40:17 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Apr 27 17:48:17 2006 +0200
     1.3 @@ -200,10 +200,10 @@
     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 -                [((cl_name^"1", axiom1),[Simplifier.simp_add]), 
     1.9 -                 ((cl_name^"2", axiom2),[]),                           
    1.10 -                 ((cl_name^"3", axiom3),[])] thy                          
    1.11 +          AxClass.add_axclass_i (cl_name, ["HOL.type"]) []
    1.12 +                [((cl_name ^ "1", [Simplifier.simp_add]), [axiom1]),
    1.13 +                 ((cl_name ^ "2", []), [axiom2]),                           
    1.14 +                 ((cl_name ^ "3", []), [axiom3])] thy                          
    1.15        end) ak_names_types thy6;
    1.16  
    1.17      (* proves that every pt_<ak>-type together with <ak>-type *)
    1.18 @@ -249,7 +249,7 @@
    1.19            val axiom1   = HOLogic.mk_Trueprop (HOLogic.mk_mem (csupp $ x, cfinites));
    1.20  
    1.21         in  
    1.22 -        AxClass.add_axclass_i (cl_name, [pt_name]) [((cl_name^"1", axiom1),[])] thy            
    1.23 +        AxClass.add_axclass_i (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy            
    1.24         end) ak_names_types thy8; 
    1.25  
    1.26       (* proves that every fs_<ak>-type together with <ak>-type   *)
    1.27 @@ -298,7 +298,7 @@
    1.28  			   (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
    1.29                                             cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
    1.30  	       in  
    1.31 -		 AxClass.add_axclass_i (cl_name, ["HOL.type"]) [((cl_name^"1", ax1),[])] thy'  
    1.32 +		 AxClass.add_axclass_i (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy'  
    1.33  	       end) ak_names_types thy) ak_names_types thy12;
    1.34  
    1.35          (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem;     *)