diff -r 89c55d36980f -r bcf558c445a4 Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Wed Dec 08 13:05:04 2010 +0000
+++ b/Nominal/nominal_library.ML	Wed Dec 08 13:16:25 2010 +0000
@@ -65,6 +65,11 @@
 
   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
 
@@ -209,6 +214,14 @@
   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 *)
 
 fun fresh_args ctxt f =
@@ -225,6 +238,12 @@
 (* constructor infos *)
 type cns_info = (term * typ * typ list * bool list) list
 
+(*  - term for constructor constant
+    - type of the constructor
+    - types of the arguments
+    - flags indicating whether the argument is recursive
+*)
+
 (* returns the type of the nth datatype *)
 fun all_dtyps descr sorts = 
   map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1))