--- a/Nominal/Fv.thy	Tue Mar 09 21:22:22 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 10 08:44:19 2010 +0100
@@ -215,6 +215,9 @@
     "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);
   fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =
     let
       val Ts = map (typ_of_dtyp descr sorts) dts;