--- a/src/HOL/Nominal/nominal_atoms.ML Sat Apr 07 11:36:35 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Sat Apr 07 12:40:32 2007 +0200
@@ -695,8 +695,6 @@
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";
val dj_supp = thm "Nominal.dj_supp";
val fresh_left_ineq = thm "Nominal.pt_fresh_left_ineq";