diff -r 6ab8c46b3b4b -r 7ae031bd5d2f Nominal/Fv.thy
--- a/Nominal/Fv.thy	Wed Mar 03 17:51:47 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 04 10:59:52 2010 +0100
@@ -184,8 +184,8 @@
               val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis;
               val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"})
             in
-              if length pi_supps > 1 then
-                HOLogic.mk_conj (alpha_gen, pi_supps_eq) else alpha_gen
+              (*if length pi_supps > 1 then
+                HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) alpha_gen
             (* TODO Add some test that is makes sense *)
             end else @{term "True"}
         end