--- a/src/HOL/Nominal/nominal_thmdecls.ML Wed Jan 21 16:51:45 2009 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Wed Jan 21 18:27:43 2009 +0100
@@ -187,8 +187,8 @@
"equivariance theorem declaration (without checking the form of the lemma)"),
("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"),
("bij", Attrib.add_del_args bij_add bij_del, "bijection theorem declaration")] #>
- PureThy.add_thms_dynamic ("eqvts", #eqvts o Data.get) #>
- PureThy.add_thms_dynamic ("freshs", #freshs o Data.get) #>
- PureThy.add_thms_dynamic ("bijs", #bijs o Data.get);
+ PureThy.add_thms_dynamic (Binding.name "eqvts", #eqvts o Data.get) #>
+ PureThy.add_thms_dynamic (Binding.name "freshs", #freshs o Data.get) #>
+ PureThy.add_thms_dynamic (Binding.name "bijs", #bijs o Data.get);
end;