diff -r 2fcd18e7bb18 -r b7d259ded92e Quot/Nominal/LamEx.thy
--- a/Quot/Nominal/LamEx.thy	Sat Jan 30 12:12:52 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Mon Feb 01 09:56:32 2010 +0100
@@ -548,7 +548,7 @@
 
 lemma app_supp:
   shows "supp (App t1 t2) = (supp t1) \<union> (supp t2)"
-apply(simp only: permute_lam supp_def lam_inject)
+apply(simp only: supp_def lam_inject)
 apply(simp add: Collect_imp_eq Collect_neg_eq)
 done