--- a/Nominal/Abs.thy	Tue Aug 31 21:03:08 2010 +0800
+++ b/Nominal/Abs.thy	Thu Sep 02 01:16:26 2010 +0800
@@ -368,7 +368,7 @@
 
 end
 
-lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst
+lemmas permute_abs[eqvt] = permute_Abs permute_Abs_res permute_Abs_lst
 
 
 lemma abs_swap1: