src/HOL/Nominal/nominal_atoms.ML
changeset 28083 103d9282a946
parent 28011 90074908db16
child 28372 291e7a158e95
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Sep 02 14:10:32 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Sep 02 14:10:45 2008 +0200
     1.3 @@ -265,9 +265,9 @@
     1.4                          HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
     1.5        in
     1.6            AxClass.define_class (cl_name, ["HOL.type"]) []
     1.7 -                [((cl_name ^ "1", [Simplifier.simp_add]), [axiom1]),
     1.8 -                 ((cl_name ^ "2", []), [axiom2]),                           
     1.9 -                 ((cl_name ^ "3", []), [axiom3])] thy                          
    1.10 +                [((Name.binding (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
    1.11 +                 ((Name.binding (cl_name ^ "2"), []), [axiom2]),                           
    1.12 +                 ((Name.binding (cl_name ^ "3"), []), [axiom3])] thy
    1.13        end) ak_names_types thy6;
    1.14  
    1.15      (* proves that every pt_<ak>-type together with <ak>-type *)
    1.16 @@ -313,7 +313,7 @@
    1.17            val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
    1.18  
    1.19         in  
    1.20 -        AxClass.define_class (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy            
    1.21 +        AxClass.define_class (cl_name, [pt_name]) [] [((Name.binding (cl_name ^ "1"), []), [axiom1])] thy            
    1.22         end) ak_names_types thy8; 
    1.23           
    1.24       (* proves that every fs_<ak>-type together with <ak>-type   *)
    1.25 @@ -362,7 +362,8 @@
    1.26                             (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
    1.27                                             cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
    1.28                 in  
    1.29 -                 AxClass.define_class (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy'  
    1.30 +                 AxClass.define_class (cl_name, ["HOL.type"]) []
    1.31 +                   [((Name.binding (cl_name ^ "1"), []), [ax1])] thy'  
    1.32                 end) ak_names_types thy) ak_names_types thy12;
    1.33  
    1.34          (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem;     *)