diff -r 40ade470e319 -r c8b5133045f3 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sat Apr 07 11:05:25 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Apr 07 11:36:35 2007 +0200
@@ -694,6 +694,7 @@
        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_swap_simps       = thms "Nominal.at_swap_simps";
        val swap_simp_a         = thm "swap_simp_a";
        val swap_simp_b         = thm "swap_simp_b";
        val at_supp             = thm "Nominal.at_supp";
@@ -787,6 +788,7 @@
 	    |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
             ||>> PureThy.add_thmss [(("alpha'", inst_pt_at [abs_fun_eq']),[])]
             ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])]
+            ||>> PureThy.add_thmss [(("swap_simps", inst_at at_swap_simps),[])]	 
             ||>> PureThy.add_thmss 
 	      let val thms1 = inst_pt_at [pt_pi_rev];
 		  val thms2 = inst_pt_at [pt_rev_pi];
@@ -802,8 +804,6 @@
             ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
             ||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
             ||>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])]
-            ||>> PureThy.add_thmss [(("swap_simp_a", inst_at [swap_simp_a]),[])]	 
-            ||>> PureThy.add_thmss [(("swap_simp_b", inst_at [swap_simp_b]),[])]
             ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[NominalThmDecls.eqvt_add])] 
             ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_add])]
             ||>> PureThy.add_thmss