--- a/Nominal/Fv.thy	Wed Mar 10 10:11:20 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 10 10:47:21 2010 +0100
@@ -234,7 +234,7 @@
   val (_, (_, _, constrs)) = nth descr ith_dtyp;
   val eqs = map2i alpha_bn_constr constrs args_in_bns
 in
-  ((bn, alpha_bn_name), (alpha_bn_free, eqs))
+  ((bn, alpha_bn_free), (alpha_bn_name, eqs))
 end
 *}
 
@@ -261,9 +261,10 @@
   val alpha_frees = map Free (alpha_names ~~ alpha_types);
   (* We assume that a bn is either recursive or not *)
   val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns;
-
-  val alpha_bnfrees = map (fst o snd) (map (alpha_bn thy dt_info alpha_frees) (bns ~~ bns_rec))
-
+  val (bn_alpha_bns, alpha_bn_names_eqs) = split_list (map (alpha_bn thy dt_info alpha_frees) (bns ~~ bns_rec))
+  val (alpha_bn_names, alpha_bn_eqs) = split_list alpha_bn_names_eqs;
+  val alpha_bn_frees = map snd bn_alpha_bns;
+  val alpha_bn_types = map fastype_of alpha_bn_frees;
   fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =
     let
       val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -329,7 +330,7 @@
             (* TODO: if more then check and accept *)
           | (_, [], []) => @{term True}
           | ([], [(((SOME (bn, _)), _, _), pi)], []) =>
-              nth alpha_bnfrees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2
+              nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2
           | ([], [], relevant) =>
             let
               val (rbinds, rpis) = split_list relevant
@@ -380,8 +381,9 @@
   val (alphas, lthy''') = (Inductive.add_inductive_i
      {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'')
+     (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) (alpha_names @ alpha_bn_names)
+     (alpha_types @ alpha_bn_types)) []
+     (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'')
   val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2)
 in
   ((all_fvs, alphas), lthy''')
@@ -390,29 +392,24 @@
 
 (*
 atom_decl name
-
 datatype lam =
   VAR "name"
 | APP "lam" "lam"
 | LET "bp" "lam"
 and bp =
   BP "name" "lam"
-
 primrec
   bi::"bp \<Rightarrow> atom set"
 where
   "bi (BP x t) = {atom x}"
-
 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *}
-
-
 local_setup {*
   snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam")
-  [[[], [], [(SOME (@{term bi}, false), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *}
+  [[[], [], [(SOME (@{term bi}, true), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *}
 print_theorems
 *)
 
-(*
+(*atom_decl name
 datatype rtrm1 =
   rVr1 "name"
 | rAp1 "rtrm1" "rtrm1"
@@ -422,24 +419,38 @@
   BUnit
 | BVr "name"
 | BPr "bp" "bp"
-
-(* to be given by the user *)
-
 primrec
   bv1
 where
   "bv1 (BUnit) = {}"
 | "bv1 (BVr x) = {atom x}"
 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
-
-setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Fv.rtrm1", "Fv.bp"] *}
-
-local_setup {* define_fv_alpha "Fv.rtrm1"
-  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
-   [[], [[]], [[], []]]] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm1") 2 *}
+local_setup {*
+  snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm1")
+  [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, false), 0, 2)]],
+  [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *}
 print_theorems
 *)
 
+(*
+atom_decl name
+datatype rtrm5 =
+  rVr5 "name"
+| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
+and rlts =
+  rLnil
+| rLcons "name" "rtrm5" "rlts"
+primrec
+  rbv5
+where
+  "rbv5 rLnil = {}"
+| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm5") 2 *}
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm5")
+  [[[], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *}
+print_theorems
+*)
 
 ML {*
 fun alpha_inj_tac dist_inj intrs elims =