diff -r 65bdcc42badd -r 2725853f43b9 Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Tue May 04 17:25:58 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Wed May 05 10:24:54 2010 +0100
@@ -384,6 +384,12 @@
 apply(perm_simp exclude: The)
 oops
 
+lemma 
+  fixes P :: "(('b \<Rightarrow> bool) \<Rightarrow> ('b::pt)) \<Rightarrow> ('a::pt)"
+  shows "(p \<bullet> (P The)) = foo"
+apply(perm_simp exclude: The)
+oops
+
 thm eqvts
 thm eqvts_raw