--- a/Nominal/Fv.thy	Mon Mar 08 10:33:55 2010 +0100
+++ b/Nominal/Fv.thy	Mon Mar 08 11:10:43 2010 +0100
@@ -209,7 +209,7 @@
               val rhs = mk_pair (rhs_binds, arg2);
               val alpha = nth alpha_frees (body_index dt);
               val fv = nth fv_frees (body_index dt);
-              val pi = foldr1 add_perm rpis;
+              val pi = foldr1 add_perm (distinct (op =) rpis);
               val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
               val alpha_gen = Syntax.check_term lthy alpha_gen_pre
 (*              val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis;