--- a/src/HOL/Nominal/nominal_permeq.ML Fri Apr 06 01:26:30 2007 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Sat Apr 07 11:05:25 2007 +0200
@@ -153,7 +153,7 @@
end);
(* general simplification of permutations and permutation that arose from eqvt-problems *)
-val perm_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp"] (fn st => []);
+val perm_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simp_a","swap_simp_b"] (fn st => []);
val eqvt_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_pi_simp"] eqvts_thms;
(* FIXME removes the name lookup for these theorems use an ml value instead *)