src/HOL/Nominal/nominal_atoms.ML

       val pt3           = thm "pt3";
       val at_pt_inst    = thm "at_pt_inst";
       val pt_set_inst   = thm "pt_set_inst"; 
       val pt_unit_inst  = thm "pt_unit_inst";
       val pt_prod_inst  = thm "pt_prod_inst"; 
+      val pt_nprod_inst = thm "pt_nprod_inst"; 
       val pt_list_inst  = thm "pt_list_inst";   
       val pt_optn_inst  = thm "pt_option_inst";   
       val pt_noptn_inst = thm "pt_noption_inst";   
       val pt_fun_inst   = thm "pt_fun_inst";     
 

      (*      fun(pt_<ak>,pt_<ak>)       *)
      (*      noption(pt_<ak>)           *)
      (*      option(pt_<ak>)            *)
      (*      list(pt_<ak>)              *)
      (*      *(pt_<ak>,pt_<ak>)         *)
+     (*      nprod(pt_<ak>,pt_<ak>)     *)
      (*      unit                       *)
      (*      set(pt_<ak>)               *)
      (* are instances of pt_<ak>        *)
      val thy18 = fold (fn ak_name => fn thy =>
        let

           val pt_thm_fun   = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst));
           val pt_thm_noptn = pt_inst RS pt_noptn_inst; 
           val pt_thm_optn  = pt_inst RS pt_optn_inst; 
           val pt_thm_list  = pt_inst RS pt_list_inst;
           val pt_thm_prod  = pt_inst RS (pt_inst RS pt_prod_inst);
+          val pt_thm_nprod = pt_inst RS (pt_inst RS pt_nprod_inst);
           val pt_thm_unit  = pt_unit_inst;
           val pt_thm_set   = pt_inst RS pt_set_inst
        in 
 	thy
 	|> AxClass.add_inst_arity_i ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
         |> AxClass.add_inst_arity_i ("nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
         |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
         |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
         |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
+        |> AxClass.add_inst_arity_i ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
+                                    (pt_proof pt_thm_nprod)
         |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
         |> AxClass.add_inst_arity_i ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
      end) ak_names thy13; 
 
        (*<<<<<<<  fs_<ak> class instances  >>>>>>>*)

        (* abbreviations for some lemmas *)
        val fs1            = thm "fs1";
        val fs_at_inst     = thm "fs_at_inst";
        val fs_unit_inst   = thm "fs_unit_inst";
        val fs_prod_inst   = thm "fs_prod_inst";
+       val fs_nprod_inst  = thm "fs_nprod_inst";
        val fs_list_inst   = thm "fs_list_inst";
        val fs_option_inst = thm "fs_option_inst";
        val dj_supp        = thm "dj_supp"
 
        (* shows that <ak> is an instance of fs_<ak>     *)

         end) ak_names thy) ak_names thy18;
 
        (* shows that                  *)
        (*    unit                     *)
        (*    *(fs_<ak>,fs_<ak>)       *)
+       (*    nprod(fs_<ak>,fs_<ak>)   *)
        (*    list(fs_<ak>)            *)
        (*    option(fs_<ak>)          *) 
        (* are instances of fs_<ak>    *)
 
        val thy24 = fold (fn ak_name => fn thy => 
         let
           val cls_name = Sign.full_name (sign_of thy) ("fs_"^ak_name);
           val fs_inst  = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
           fun fs_proof thm = EVERY [AxClass.intro_classes_tac [], rtac (thm RS fs1) 1];      
 
-          val fs_thm_unit = fs_unit_inst;
-          val fs_thm_prod = fs_inst RS (fs_inst RS fs_prod_inst);
-          val fs_thm_list = fs_inst RS fs_list_inst;
-          val fs_thm_optn = fs_inst RS fs_option_inst;
+          val fs_thm_unit  = fs_unit_inst;
+          val fs_thm_prod  = fs_inst RS (fs_inst RS fs_prod_inst);
+          val fs_thm_nprod = fs_inst RS (fs_inst RS fs_nprod_inst);
+          val fs_thm_list  = fs_inst RS fs_list_inst;
+          val fs_thm_optn  = fs_inst RS fs_option_inst;
         in 
          thy 
          |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
-         |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)    
+         |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
+         |> AxClass.add_inst_arity_i ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
+                                     (fs_proof fs_thm_nprod) 
          |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
          |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
         end) ak_names thy20; 
 
        (*<<<<<<<  cp_<ak>_<ai> class instances  >>>>>>>*)