Quot/Nominal/nominal_thmdecls.ML
changeset 1039 0d832c36b1bb
parent 1037 2845e736dc1a
child 1059 090fa3f21380
--- 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;