--- a/src/HOL/Nominal/nominal_atoms.ML Thu Apr 27 17:40:17 2006 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Thu Apr 27 17:48:17 2006 +0200
@@ -200,10 +200,10 @@
(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"])
- [((cl_name^"1", axiom1),[Simplifier.simp_add]),
- ((cl_name^"2", axiom2),[]),
- ((cl_name^"3", axiom3),[])] thy
+ AxClass.add_axclass_i (cl_name, ["HOL.type"]) []
+ [((cl_name ^ "1", [Simplifier.simp_add]), [axiom1]),
+ ((cl_name ^ "2", []), [axiom2]),
+ ((cl_name ^ "3", []), [axiom3])] thy
end) ak_names_types thy6;
(* proves that every pt_<ak>-type together with <ak>-type *)
@@ -249,7 +249,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.add_axclass_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 *)
@@ -298,7 +298,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.add_axclass_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; *)