
diff -r 9f44608ea28d -r 445518561867 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Wed Apr 06 13:47:08 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Fri Apr 08 03:47:50 2011 +0800
@@ -733,7 +733,7 @@
 
 lemma eqvt_lambda:
   fixes f :: "'a::pt \<Rightarrow> 'b::pt"
-  shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
+  shows "p \<bullet> f \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
   unfolding permute_fun_def unpermute_def by simp
 
 lemma eqvt_bound:




