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