src/HOL/Nominal/nominal_atoms.ML

        val pt_bij              = thm "Nominal.pt_bij";
        val pt_perm_compose     = thm "Nominal.pt_perm_compose";
        val pt_perm_compose'    = thm "Nominal.pt_perm_compose'";
        val perm_app            = thm "Nominal.pt_fun_app_eq";
        val at_fresh            = thm "Nominal.at_fresh";
+       val at_fresh_ineq       = thm "Nominal.at_fresh_ineq";
        val at_calc             = thms "Nominal.at_calc";
        val at_supp             = thm "Nominal.at_supp";
        val dj_supp             = thm "Nominal.dj_supp";
        val fresh_left_ineq     = thm "Nominal.pt_fresh_left_ineq";
        val fresh_left          = thm "Nominal.pt_fresh_left";

        val fresh_right         = thm "Nominal.pt_fresh_right";
        val fresh_bij_ineq      = thm "Nominal.pt_fresh_bij_ineq";
        val fresh_bij           = thm "Nominal.pt_fresh_bij";
        val fresh_aux_ineq      = thm "Nominal.pt_fresh_aux_ineq";
        val fresh_aux           = thm "Nominal.pt_fresh_aux";
+       val fresh_eqvt          = thm "Nominal.pt_fresh_eqvt";
+       val all_eqvt            = thm "Nominal.pt_all_eqvt";
        val pt_pi_rev           = thm "Nominal.pt_pi_rev";
        val pt_rev_pi           = thm "Nominal.pt_rev_pi";
+       val at_exists_fresh     = thm "Nominal.at_exists_fresh";
   
 
        (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
        (* types; this allows for example to use abs_perm (which is a      *)
        (* collection of theorems) instead of thm abs_fun_pi with explicit *)

 		  val thms2 = instR cp1 (Library.flat cps');
               in [(("perm_compose",thms1 @ thms2),[])] end
             ||>> PureThy.add_thmss [(("perm_compose'",inst_pt_at [pt_perm_compose']),[])] 
             ||>> PureThy.add_thmss [(("perm_app", inst_pt_at [perm_app]),[])]
             ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
-            ||>> PureThy.add_thmss [(("fresh_atm", inst_at [at_fresh]),[])]
+            ||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
+            ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[])]
+            ||>> PureThy.add_thmss 
+	      let val thms1 = inst_at [at_fresh]
+		  val thms2 = inst_dj [at_fresh_ineq]
+	      in [(("fresh_atm", thms1 @ thms2),[])] end
             ||>> PureThy.add_thmss [(("calc_atm", inst_at at_calc),[])]
             ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [abs_fun_pi]
 		  and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq]
 	      in [(("abs_perm", thms1 @ thms2),[])] end

 		  and thms2 = inst_pt_pt_at_cp [fresh_right_ineq]
 	      in [(("fresh_right", thms1 @ thms2),[])] end
             ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [fresh_bij]
 		  and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq]
-	      in [(("fresh_eqvt", thms1 @ thms2),[])] end
+	      in [(("fresh_bij", thms1 @ thms2),[])] end
+            ||>> PureThy.add_thmss
+	      let val thms1 = inst_pt_at [fresh_eqvt]
+	      in [(("fresh_eqvt", thms1),[])] end
             ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [fresh_aux]
 		  and thms2 = inst_pt_pt_at_cp_dj [fresh_aux_ineq]
 	      in [(("fresh_aux", thms1 @ thms2),[])] end
 	   end;