# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268043043 -3600
# Node ID 3bf496a971c618aeceee41fc18de124641c3816e
# Parent  0c843fcb1d7b0ff6514aaa8301705eb42c466639
Fix permutation addition.

diff -r 0c843fcb1d7b -r 3bf496a971c6 Nominal/Fv.thy
--- 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;