diff -r be512c15daa5 -r 205ac2d13339 Nominal/Perm.thy
--- a/Nominal/Perm.thy	Tue May 04 06:05:13 2010 +0100
+++ b/Nominal/Perm.thy	Tue May 04 06:24:54 2010 +0100
@@ -113,15 +113,14 @@
 (* defines the permutation functions for raw datatypes and
    proves that they are instances of pt
 
-   dt_nos refers to the number of "un-unfolded" datatypes
+   user_dt_nos refers to the number of "un-unfolded" datatypes
    given by the user
 *)
-fun define_raw_perms (dt_info : Datatype_Aux.info) thy =
+fun define_raw_perms (dt_info : Datatype_Aux.info) user_dt_nos thy =
 let
   val {descr as dt_descr, induct, sorts, ...} = dt_info;
-  val dt_nos = length dt_descr
   val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;
-  val full_tnames = List.take (all_full_tnames, dt_nos);
+  val user_full_tnames = List.take (all_full_tnames, user_dt_nos);
 
   val perm_fn_names = prefix_dt_names dt_descr sorts "permute_"
 
@@ -135,7 +134,7 @@
   val perm_eqs = maps perm_eq dt_descr;
 
   val lthy =
-    Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
+    Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy;
    
   val ((perm_fns, perm_ldef), lthy') =
     Primrec.add_primrec
@@ -143,8 +142,8 @@
     
   val perm_zero_thms = prove_permute_zero lthy' induct perm_ldef perm_fns
   val perm_plus_thms = prove_permute_plus lthy' induct perm_ldef perm_fns
-  val perm_zero_thms' = List.take (perm_zero_thms, dt_nos);
-  val perm_plus_thms' = List.take (perm_plus_thms, dt_nos)
+  val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos);
+  val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos)
   val perms_name = space_implode "_" perm_fn_names
   val perms_zero_bind = Binding.name (perms_name ^ "_zero")
   val perms_plus_bind = Binding.name (perms_name ^ "_plus")