--- a/Nominal/Fv.thy	Wed Mar 10 09:58:43 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 10 10:11:20 2010 +0100
@@ -213,8 +213,18 @@
     val rhs = HOLogic.mk_Trueprop
       (alpha_bn_free $ pi $ (list_comb (c, args)) $ (list_comb (c, args2)));
     fun lhs_arg ((dt, arg_no), (arg, arg2)) =
-      (*...*)
-      @{term True}
+      let
+        val argty = fastype_of arg;
+        val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty);
+        val permarg = if is_rec then permute $ pi $ arg else arg
+      in
+      if is_rec_type dt then
+        if arg_no mem args_in_bn then alpha_bn_free $ pi $ arg $ arg2
+        else (nth alpha_frees (body_index dt)) $ permarg $ arg2
+      else
+        if arg_no mem args_in_bn then @{term True}
+        else HOLogic.mk_eq (permarg, arg2)
+      end
     val arg_nos = 0 upto (length dts - 1)
     val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2)))
     val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs)