--- a/Nominal/Perm.thy	Thu Mar 18 10:12:41 2010 +0100
+++ b/Nominal/Perm.thy	Thu Mar 18 10:15:57 2010 +0100
@@ -96,7 +96,6 @@
     val perm_eqs = maps perm_eq descr;
     val lthy =
       Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
-    (* TODO: Use the version of prmrec that gives the names explicitely. *)
     val ((perm_frees, perm_ldef), lthy') =
       Primrec.add_primrec
         (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy;

--- a/TODO	Thu Mar 18 10:12:41 2010 +0100
+++ b/TODO	Thu Mar 18 10:15:57 2010 +0100
@@ -21,3 +21,10 @@
 
 - automate the proofs that are currently proved with sorry:
   alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp
+
+- store information about defined nominal datatypes, so that
+  it can be used to define new types that depend on these
+
+- make 3 versions of Abs
+
+- make parser aware of recursive and of different versions of abs