Adapted to new interface of add_axclass_i.

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