--- a/Nominal/Ex/Let.thy	Wed Jun 29 16:44:54 2011 +0100
+++ b/Nominal/Ex/Let.thy	Wed Jun 29 17:01:09 2011 +0100
@@ -129,12 +129,6 @@
 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)"
   by (simp add: permute_pure)
 
-(* TODO: should be provided by nominal *)
-lemmas [eqvt] = trm_assn.fv_bn_eqvt
-thm trm_assn.fv_bn_eqvt
-
-
-thm Abs_lst_fcb
 
 lemma Abs_lst_fcb2:
   fixes as bs :: "'a :: fs"