diff -r bcf558c445a4 -r 90779aefbf1a Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Wed Dec 08 13:16:25 2010 +0000
+++ b/Nominal/nominal_library.ML	Wed Dec 08 17:07:08 2010 +0000
@@ -65,11 +65,6 @@
 
   val to_set: term -> term
 
-  (* some attributes *)
-  val eqvt_attr : Args.src
-  val rsp_attr  : Args.src
-  val simp_attr : Args.src
-
   (* fresh arguments for a term *)
   val fresh_args: Proof.context -> term -> term list
 
@@ -214,12 +209,6 @@
   else t
 
 
-(* some frequently used 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)
-
 
 
 (* produces fresh arguments for a term *)