--- a/Nominal/Nominal2.thy	Wed Dec 08 13:05:04 2010 +0000
+++ b/Nominal/Nominal2.thy	Wed Dec 08 13:16:25 2010 +0000
@@ -18,14 +18,6 @@
 
 section{* Interface for nominal_datatype *}
 
-ML {*
-(* attributes *)
-val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
-val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)
-val simp_attr = Attrib.internal (K Simplifier.simp_add)
-
-*}
-
 ML {* print_depth 50 *}
 
 ML {*