--- 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