--- a/src/HOL/Nominal/Examples/Lam_Funs.thy Wed Mar 28 10:47:19 2007 +0200
+++ b/src/HOL/Nominal/Examples/Lam_Funs.thy Wed Mar 28 17:27:44 2007 +0200
@@ -64,7 +64,7 @@
apply(fresh_guess)+
done
-lemma subst_eqvt[simp]:
+lemma subst_eqvt[eqvt]:
fixes pi:: "name prm"
and t1:: "lam"
and t2:: "lam"