diff -r 837b889fcf59 -r 3622cae9b10e Nominal/Perm.thy
--- 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 {*