diff -r c8acaded1777 -r 4a00077c008f Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue Jul 19 19:09:06 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Fri Jul 22 11:37:16 2011 +0100
@@ -644,8 +644,8 @@
   apply (simp add: finite_supp)
   apply (simp add: fresh_Inl var_fresh_subst)
   apply(simp add: fresh_star_def)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt)
 done