--- a/src/HOL/Nominal/nominal_permeq.ML Wed Mar 28 17:27:44 2007 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Wed Mar 28 18:25:23 2007 +0200
@@ -151,7 +151,7 @@
(* 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"];
-val eqvt_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_pi_simp","eqvt"];
+val eqvt_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_pi_simp","eqvts"];
(* main simplification tactics for permutations *)
(* FIXME: perm_simp_tac should simplify more permutations *)