# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267560604 -3600
# Node ID acf262971303b7791050ac5e717dd7b8b34b47f3
# Parent  12ce0167318801f32598268af7b0aebe64477ac9
Fixes for the fv problem and alpha problem.

diff -r 12ce01673188 -r acf262971303 Nominal/Fv.thy
--- 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);