--- a/Nominal/Fv.thy	Mon Mar 15 23:42:56 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 16 12:06:22 2010 +0100
@@ -341,7 +341,8 @@
               val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty)
             in
               if bns_same rel_in_comp_binds then
-                HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2)))
+                alpha_bn
+(*                HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2)))*)
               else error "incompatible bindings for one argument"
             end
           | ([], [], relevant) =>