diff -r c6db12ddb60c -r c785fff02a8f Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Thu May 27 18:37:52 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Thu May 27 18:40:10 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)