# HG changeset patch
# User urbanc
# Date 1133955218 -3600
# Node ID 0040ee0b01c984516541ce87f7a58ff192645450
# Parent  e8b7e0a2272780ffeee64382e9f4c50be1a00b49
tuned

diff -r e8b7e0a22727 -r 0040ee0b01c9 src/HOL/Nominal/Examples/Lam_substs.thy
--- 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)