# HG changeset patch
# User urbanc
# Date 1175942432 -7200
# Node ID 0e008e3ddb1e5c4b43a43d37421f380aa8ee5721
# Parent  c8b5133045f396a57ff8b729933bf03aabf36f92
deleted remaining instances of swap_simp_a and swap_simp_b (obsolete now)

diff -r c8b5133045f3 -r 0e008e3ddb1e src/HOL/Nominal/nominal_atoms.ML
--- 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";