--- a/Nominal/NewParser.thy	Tue May 04 06:05:13 2010 +0100
+++ b/Nominal/NewParser.thy	Tue May 04 06:24:54 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) lthy1;
+    Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) 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);