--- a/Nominal/Perm.thy	Tue Apr 20 08:45:53 2010 +0200
+++ b/Nominal/Perm.thy	Tue Apr 20 08:57:13 2010 +0200
@@ -70,29 +70,18 @@
 ML {*
 (* permutation function for one argument 
    
-    - in case the argument is non-recursive it returns 
+    - in case the argument is recursive it returns 
+
+         permute_fn p arg
+
+    - in case the argument is non-recursive it will build
 
          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) =
   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, permute_fn $ pi $ 
-        list_comb (arg, map (fn (i, U) => (mk_perm_ty U (mk_minus pi) (Bound i))) indxs_tys))
-    end
+  then Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ pi $ arg
   else mk_perm pi arg
 *}