--- a/Nominal/Fv.thy	Wed Mar 10 10:47:21 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 10 11:19:59 2010 +0100
@@ -330,7 +330,13 @@
             (* TODO: if more then check and accept *)
           | (_, [], []) => @{term True}
           | ([], [(((SOME (bn, _)), _, _), pi)], []) =>
-              nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2
+            let
+              val alpha_bn = nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2
+              val ty = fastype_of (bn $ arg)
+              val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty)
+            in
+              HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2)))
+            end
           | ([], [], relevant) =>
             let
               val (rbinds, rpis) = split_list relevant