25          permute_fn p arg

    25          permute_fn p arg

    26 

    26 

    27     - in case the argument is non-recursive it will return

    27     - in case the argument is non-recursive it will return

    28 

    28 

    29          p o arg

    29          p o arg

    31 *)

    30 *)

    32 fun perm_arg permute_fn_frees p (arg_dty, arg) =

    31 fun perm_arg permute_fn_frees p (arg_dty, arg) =

    33   if Datatype_Aux.is_rec_type arg_dty 

    32   if Datatype_Aux.is_rec_type arg_dty 

    34   then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg

    33   then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg

    35   else mk_perm p arg

    34   else mk_perm p arg