--- a/Nominal/Ex/Foo2.thy	Wed Dec 08 13:05:04 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Wed Dec 08 13:16:25 2010 +0000
@@ -76,7 +76,6 @@
   (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm)
 *}
 
-
 ML {*
   @{thms foo.exhaust}
   |> map prop_of

--- 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 {*

--- 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))