--- a/Nominal/Fv.thy	Wed Mar 10 09:36:07 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 10 09:45:38 2010 +0100
@@ -201,9 +201,20 @@
   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);
-(*... *)
+  fun alpha_bn_constr (cname, dts) args_in_bn =
+  let
+    val Ts = map (typ_of_dtyp descr sorts) dts;
+    val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
+    val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);
+    val args = map Free (names ~~ Ts);
+    val args2 = map Free (names2 ~~ Ts);
+    val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
+    (*...*)
+  in
+    []
+  end
   val (_, (_, _, constrs)) = nth descr ith_dtyp;
-  val eqs = [] (*map2i alpha_bn_constr constrs args_in_bns*)
+  val eqs = map2i alpha_bn_constr constrs args_in_bns
 in
   ((bn, alpha_bn_name), (alpha_bn_free, eqs))
 end