--- a/src/HOL/Nominal/Examples/Lam_substs.thy Tue Dec 06 17:26:26 2005 +0100
+++ b/src/HOL/Nominal/Examples/Lam_substs.thy Wed Dec 07 12:33:38 2005 +0100
@@ -30,7 +30,7 @@
case (Lam a t)
have ih: "\<And>(pi::name prm) x. P x (pi\<bullet>t)" by fact
show "\<And>(pi::name prm) x. P x (pi\<bullet>(Lam [a].t))"
- proof (simp add: abs_perm)
+ proof (simp)
fix x::"'a" and pi::"name prm"
have "\<exists>c::name. c\<sharp>(f x,pi\<bullet>a,pi\<bullet>t)"
by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1 fs)