diff -r b71b838b0a75 -r 6d4e4bf9bce6 Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Fri Apr 16 11:09:32 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Fri Apr 16 16:29:11 2010 +0200
@@ -369,6 +369,7 @@
 
 text {* Problem: there is no raw eqvt-rule for The *}
 lemma "p \<bullet> (THE x. P x) = foo"
+apply(tactic {* Nominal_Permeq.eqvt_tac @{context} [] [@{const_name "The"}] 1*})
 apply(perm_simp)
 (* apply(perm_strict_simp) *)
 oops