diff -r 8e0bfb14f6bf -r 57db4ff0893b Nominal/Perm.thy
--- a/Nominal/Perm.thy	Tue Apr 20 07:44:47 2010 +0200
+++ b/Nominal/Perm.thy	Tue Apr 20 08:45:53 2010 +0200
@@ -68,23 +68,32 @@
 *}
 
 ML {*
-(* permutation function for one argument *)
+(* permutation function for one argument 
+   
+    - in case the argument is non-recursive it returns 
+
+         p o arg
+
+    - in case the argument is recursive it will build
+
+         %x1..xn. permute_fn p (arg (-p o x1)..(-p o xn))
+
+      the x1..xn depend whether the argument is of function
+      type; normally it just returns permute_fn pi arg 
+*)
 fun perm_arg permute_fns pi (arg_dty, arg) =
-let 
-  val T = type_of arg
-in
   if Datatype_Aux.is_rec_type arg_dty 
   then 
     let 
+      val T = type_of arg
       val (Us, _) = strip_type T
       val indxs_tys = (length Us - 1 downto 0) ~~ Us
+      val permute_fn = Free (nth permute_fns (Datatype_Aux.body_index arg_dty))
     in 
-      list_abs (map (pair "x") Us,
-        Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ pi $
-          list_comb (arg, map (fn (i, U) => (mk_perm_ty U (mk_minus pi) (Bound i))) indxs_tys))
+      list_abs (map (pair "x") Us, permute_fn $ pi $ 
+        list_comb (arg, map (fn (i, U) => (mk_perm_ty U (mk_minus pi) (Bound i))) indxs_tys))
     end
-  else mk_perm_ty T pi arg
-end
+  else mk_perm pi arg
 *}
 
 ML {*
@@ -152,7 +161,7 @@
 *}
 
 (* Test *)
-atom_decl name
+(*atom_decl name
 
 datatype trm =
   Var "name"