--- a/Nominal/Fv.thy	Tue Mar 02 20:14:21 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 02 21:10:04 2010 +0100
@@ -72,6 +72,7 @@
     fold (fn a => fn b =>
       if a = noatoms then b else
       if b = noatoms then a else
+      if a = b then a else
       HOLogic.mk_binop "Set.union" (a, b)) (rev sets) noatoms;
   fun mk_conjl props =
     fold (fn a => fn b =>
@@ -124,7 +125,8 @@
     let
       val Ts = map (typ_of_dtyp descr sorts) dts;
       val bindslen = length bindcs
-      val pi_strs = replicate bindslen "pi"
+      val pi_strs_same = replicate bindslen "pi"
+      val pi_strs = Name.variant_list [] pi_strs_same;
       val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs;
       val bind_pis = bindcs ~~ pis;
       val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts);