--- a/Nominal/NewParser.thy	Tue May 04 05:36:55 2010 +0100
+++ b/Nominal/NewParser.thy	Tue May 04 06:02:45 2010 +0100
@@ -374,7 +374,7 @@
 
   (* definitions of raw permutations *)
   val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
-    Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1;
+    Local_Theory.theory_result (define_raw_perms dtinfo) lthy1;
 
   val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
   fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
@@ -698,7 +698,8 @@
   (main_parser >> nominal_datatype2_cmd)
 *}
 
-(*atom_decl name
+
+atom_decl name
 
 nominal_datatype lam =
   Var name