--- a/Nominal-General/Nominal2_Eqvt.thy	Sat Sep 18 05:13:42 2010 +0800
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sat Sep 18 06:09:43 2010 +0800
@@ -74,7 +74,7 @@
 (* the normal version of this lemma would cause loops *)
 lemma permute_eqvt_raw[eqvt_raw]:
   shows "p \<bullet> permute \<equiv> permute"
-apply(simp add: expand_fun_eq permute_fun_def)
+apply(simp add: fun_eq_iff permute_fun_def)
 apply(subst permute_eqvt)
 apply(simp)
 done