diff -r 6911934c98c7 -r 0d832c36b1bb Quot/Nominal/nominal_thmdecls.ML
--- a/Quot/Nominal/nominal_thmdecls.ML	Wed Feb 03 12:13:22 2010 +0100
+++ b/Quot/Nominal/nominal_thmdecls.ML	Wed Feb 03 12:31:58 2010 +0100
@@ -113,7 +113,7 @@
   Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) 
     (cat_lines ["declaration of equivariance lemmas - they will will be", 
                 "added/deleted directly to the eqvt thm-list"]) #>
-  PureThy.add_thms_dynamic (@{binding "eqvt"}, content);
+  PureThy.add_thms_dynamic (@{binding "eqvts"}, content);
 
 
 end;