src/HOL/Nominal/nominal_atoms.ML

 fun create_nom_typedecls ak_names thy =
   let
     
     val (_,thy1) = 
     fold_map (fn ak => fn thy => 
-          let val dt = ([],ak,NoSyn,[(ak,[@{typ nat}],NoSyn)]) 
+          let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
               val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype true false [ak] [dt] thy
               val inject_flat = Library.flat inject
               val ak_type = Type (Sign.intern_type thy1 ak,[])
               val ak_sign = Sign.intern_const thy1 ak 
               

         val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
                 (cswap_akname $ HOLogic.mk_prod (a,b) $ c,
                     cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c)))
         val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
       in
-        thy |> Sign.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] 
+        thy |> Sign.add_consts_i [(Binding.name ("swap_" ^ ak_name), swapT, NoSyn)] 
             |> PureThy.add_defs_unchecked true [((Binding.name name, def2),[])]
             |> snd
             |> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]
       end) ak_names_types thy1;
     

 
         val def2 = HOLogic.mk_Trueprop (HOLogic.mk_eq
                    (Const (qu_prm_name, prmT) $ mk_Cons x xs $ a,
                     Const (swap_name, swapT) $ x $ (Const (qu_prm_name, prmT) $ xs $ a)));
       in
-        thy |> Sign.add_consts_i [(prm_name, mk_permT T --> T --> T, NoSyn)] 
+        thy |> Sign.add_consts_i [(Binding.name prm_name, mk_permT T --> T --> T, NoSyn)] 
             |> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1), []),(("", def2), [])]
       end) ak_names_types thy3;
     
     (* defines permutation functions for all combinations of atom-kinds; *)
     (* there are a trivial cases and non-trivial cases                   *)

           (* perm-eq axiom *)
           val axiom3 = Logic.mk_implies
                        (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
                         HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
       in
-          AxClass.define_class (cl_name, ["HOL.type"]) []
+          AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
                 [((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
                  ((Binding.name (cl_name ^ "2"), []), [axiom2]),                           
                  ((Binding.name (cl_name ^ "3"), []), [axiom3])] thy
       end) ak_names_types thy6;
 

           val cfinite  = Const ("Finite_Set.finite", HOLogic.mk_setT T --> HOLogic.boolT)
           
           val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
 
        in  
-        AxClass.define_class (cl_name, [pt_name]) [] [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy            
+        AxClass.define_class (Binding.name cl_name, [pt_name]) []
+          [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy
        end) ak_names_types thy8; 
          
      (* proves that every fs_<ak>-type together with <ak>-type   *)
      (* instance of fs-type                                      *)
      (* lemma abst_<ak>_inst:                                    *)

 
                val ax1   = HOLogic.mk_Trueprop 
                            (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
                                            cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
                in  
-                 AxClass.define_class (cl_name, ["HOL.type"]) []
+                 AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
                    [((Binding.name (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;     *)
         (* lemma cp_<ak1>_<ak2>_inst:                                           *)