--- a/Nominal/Fv.thy	Wed Mar 10 09:10:11 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 10 09:36:07 2010 +0100
@@ -193,6 +193,22 @@
 end
 *}
 
+ML {*
+fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees ((bn, ith_dtyp, args_in_bns), is_rec) =
+let
+  val {descr, sorts, ...} = dt_info;
+  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+  val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));
+  val alpha_bn_type = @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool}
+  val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type);
+(*... *)
+  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))
+end
+*}
+
 ML {* fn x => split_list(flat x) *}
 ML {* fn x => apsnd flat (split_list (map split_list x)) *}
 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
@@ -209,15 +225,16 @@
   val nr_bns = non_rec_binds bindsall;
   val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns;
   val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns);
-  val fv_bns = map snd bn_fv_bns;
   val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs;
   val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
     "alpha_" ^ name_of_typ (nth_dtyp i)) descr);
   val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;
   val alpha_frees = map Free (alpha_names ~~ alpha_types);
-  val alpha_bnnames = map (fn (bn, _, _) => "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)))) bns;
-  val alpha_bntypes = map (fn (_, i, _) => @{typ perm} --> nth_dtyp i --> nth_dtyp i --> @{typ bool}) bns;
-  val alpha_bnfrees = map Free (alpha_bnnames ~~ alpha_bntypes);
+  (* 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))
+
   fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =
     let
       val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -302,6 +319,7 @@
 (*              if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*)
               alpha_gen
             end
+          | _ => error "Fv.alpha: not supported binding structure"
         end
       val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2))
       val alpha_lhss = mk_conjl alphas
@@ -315,7 +333,7 @@
   val fveqs_alphaeqs = map2i fv_alpha_eq descr (gather_binds bindsall)
   val (fv_eqs_perfv, alpha_eqs) = apsnd flat (split_list (map split_list fveqs_alphaeqs))
   val rel_bns_nos = map (fn (_, i, _) => i) rel_bns;
-  fun filter_fun (a, b) = b mem rel_bns_nos;
+  fun filter_fun (_, b) = b mem rel_bns_nos;
   val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1))
   val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs)))
   val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs)))
@@ -335,8 +353,9 @@
       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'')
+  val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2)
 in
-  ((fvs, alphas), lthy''')
+  ((all_fvs, alphas), lthy''')
 end
 *}