--- a/Nominal/Fv.thy	Tue Mar 02 21:43:27 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 03 10:39:43 2010 +0100
@@ -61,7 +61,6 @@
   | map2i _ _ _ = raise UnequalLengths;
 *}
 
-(* TODO: should be const_name union *)
 ML {*
   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
   (* TODO: It is the same as one in 'nominal_atoms' *)
@@ -73,7 +72,8 @@
       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;
+      HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;
+  val mk_inter = foldr1 (HOLogic.mk_binop @{const_name inf})
   fun mk_conjl props =
     fold (fn a => fn b =>
       if a = @{term True} then b else
@@ -178,11 +178,14 @@
               val rhs = mk_pair (rhs_binds, arg2);
               val alpha = nth alpha_frees (body_index dt);
               val fv = nth fv_frees (body_index dt);
-              (* TODO: check that pis have empty intersection *)
               val pi = foldr1 add_perm 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;
+              val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"})
             in
-              Syntax.check_term lthy alpha_gen_pre
+              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
@@ -200,7 +203,7 @@
   val (fvs, lthy') = (Primrec.add_primrec
     (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy)
   val (alphas, lthy'') = (Inductive.add_inductive_i
-     {quiet_mode = false, verbose = true, alt_name = Binding.empty,
+     {quiet_mode = true, verbose = false, alt_name = Binding.empty,
       coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
      (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) []
      (add_binds alpha_eqs) [] lthy')