src/HOL/Nominal/nominal_thmdecls.ML
changeset 38808 89ae86205739
parent 38807 378ffc903bed
child 38864 4abe644fcea5
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Fri Aug 27 17:23:57 2010 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Fri Aug 27 17:59:40 2010 +0200
@@ -175,7 +175,7 @@
    "equivariance theorem declaration" #>
   Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
     "equivariance theorem declaration (without checking the form of the lemma)" #>
-  PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get);
+  PureThy.add_thms_dynamic (@{binding eqvts}, Data.get);
 
 
 end;