# 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";