--- 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"

--- a/Nominal/nominal_thmdecls.ML	Wed Jun 29 16:44:54 2011 +0100
+++ b/Nominal/nominal_thmdecls.ML	Wed Jun 29 17:01:09 2011 +0100
@@ -58,7 +58,13 @@
 val get_eqvts_thms = eqvts o  Context.Proof;
 val get_eqvts_raw_thms = eqvts_raw o Context.Proof;
 
-val add_thm = EqvtData.map o Item_Net.update;
+fun checked_update key net =
+  (if Item_Net.member net key then 
+     warning "Theorem already declared as equivariant."
+   else (); 
+   Item_Net.update key net)
+
+val add_thm = EqvtData.map o checked_update;
 val del_thm = EqvtData.map o Item_Net.remove;
 
 fun add_raw_thm thm =