--- a/Nominal/Ex/Lambda.thy	Wed Jun 01 10:59:07 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 01 11:01:39 2011 +0900
@@ -383,7 +383,7 @@
   "dblam_in None = None"
 | "dblam_in (Some x) = Some (DBLam x)"
 
-lemma [eqvt]:
+lemma db_in_eqvt[eqvt]:
   "p \<bullet> (dbapp_in x y) = dbapp_in (p \<bullet> x) (p \<bullet> y)"
   "p \<bullet> (dblam_in x) = dblam_in (p \<bullet> x)"
   apply (case_tac [!] x)