diff -r 06bf338e3215 -r b4404b13f775 Nominal/nominal_thmdecls.ML
--- 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 =