--- a/Nominal-General/Nominal2_Eqvt.thy	Thu May 27 11:21:37 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Thu May 27 18:30:26 2010 +0200
@@ -383,7 +383,7 @@
 
 declare [[trace_eqvt = false]]
 
-text {* Problem: there is no raw eqvt-rule for The *}
+text {* there is no raw eqvt-rule for The *}
 lemma "p \<bullet> (THE x. P x) = foo"
 apply(perm_strict_simp exclude: The)
 apply(perm_simp exclude: The)