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

--- a/Nominal/Perm.thy	Tue May 04 05:36:55 2010 +0100
+++ b/Nominal/Perm.thy	Tue May 04 06:02:45 2010 +0100
@@ -32,29 +32,29 @@
 
          permute_fn p arg
 
-    - in case the argument is non-recursive it will build
+    - in case the argument is non-recursive it will return
 
          p o arg
 
 *)
-fun perm_arg permute_fns pi (arg_dty, arg) =
+fun perm_arg permute_fns p (arg_dty, arg) =
   if Datatype_Aux.is_rec_type arg_dty 
-  then Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ pi $ arg
-  else mk_perm pi arg
+  then Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ p $ arg
+  else mk_perm p arg
 *}
 
 ML {*
-(* equation for permutation function for one constructor;
-   i is the index of the correspodning datatype *)
+(* generates the equation for the permutation function for one constructor;
+   i is the index of the corresponding datatype *)
 fun perm_eq_constr dt_descr sorts permute_fns i (cnstr_name, dts) =
 let
-  val pi = Free ("p", @{typ perm})
+  val p = Free ("p", @{typ perm})
   val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts
   val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
   val args = map Free (arg_names ~~ arg_tys)
   val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i))
-  val lhs = Free (nth permute_fns i) $ pi $ list_comb (cnstr, args)
-  val rhs = list_comb (cnstr, map (perm_arg permute_fns pi) (dts ~~ args))
+  val lhs = Free (nth permute_fns i) $ p $ list_comb (cnstr, args)
+  val rhs = list_comb (cnstr, map (perm_arg permute_fns p) (dts ~~ args))
   val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
 in
   (Attrib.empty_binding, eq)
@@ -116,9 +116,10 @@
    dt_nos refers to the number of "un-unfolded" datatypes
    given by the user
 *)
-fun define_raw_perms (dt_info : Datatype_Aux.info) dt_nos thy =
+fun define_raw_perms (dt_info : Datatype_Aux.info) thy =
 let
   val {descr as dt_descr, induct, sorts, ...} = dt_info;
+  val dt_nos = length descr
   val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;
   val full_tnames = List.take (all_full_tnames, dt_nos);
 
@@ -162,6 +163,10 @@
 end
 *}
 
+
+
+
+
 (* permutations for quotient types *)
 
 ML {*