--- a/Nominal/NewFv.thy	Tue May 04 14:21:18 2010 +0200
+++ b/Nominal/NewFv.thy	Tue May 04 14:25:22 2010 +0100
@@ -4,6 +4,8 @@
 begin
 
 ML {*
+(* binding modes *)
+
 datatype bmodes =
    BEmy of int
 |  BLst of ((term option * int) list) * (int list)
@@ -243,18 +245,19 @@
 *}
 
 ML {*
-fun define_raw_fv (dt_info : Datatype_Aux.info) bn_funs bclausesss lthy =
+fun define_raw_fv dt_descr sorts bn_funs bclausesss lthy =
 let
   val thy = ProofContext.theory_of lthy;
-  val {descr as dt_descr, sorts, ...} = dt_info;
 
   val fv_names = prefix_dt_names dt_descr sorts "fv_"
-  val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) dt_descr;
+  val fv_types = map (fn (i, _) => nth_dtyp dt_descr sorts i --> @{typ "atom set"}) dt_descr;
   val fv_frees = map Free (fv_names ~~ fv_types);
 
+  (* free variables for the bn-functions *)
   val (bn_fvbn, fv_bn_names, fv_bn_eqs) =
     fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss;
 
+  
   val fv_bns = map snd bn_fvbn;
   val fv_nums = 0 upto (length fv_frees - 1)