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;