--- a/Nominal/NewFv.thy	Wed Apr 28 06:40:10 2010 +0200
+++ b/Nominal/NewFv.thy	Wed Apr 28 06:55:07 2010 +0200
@@ -153,7 +153,7 @@
 *}
 
 ML {*
-fun fv_bns thy dt_info fv_frees bns bmlll =
+fun fv_bns thy dt_info fv_frees bn_funs bclauses =
 let
   fun mk_fvbn_free (bn, ith, _) =
     let
@@ -161,12 +161,12 @@
     in
       (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith)))
     end;
-  val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bns);
-  val bn_fvbn = (map (fn (bn, _, _) => bn) bns) ~~ fvbn_frees
-  val bmlls = map (fn (_, i, _) => nth bmlll i) bns;
-  val eqs = map2 (fv_bn thy dt_info fv_frees bn_fvbn) bmlls (fvbn_frees ~~ bns);
+  val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs);
+  val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees
+  val bmlls = map (fn (_, i, _) => nth bclauses i) bn_funs;
+  val eqs = map2 (fv_bn thy dt_info fv_frees bn_fvbn) bmlls (fvbn_frees ~~ bn_funs);
 in
-  (bn_fvbn, (fvbn_names, eqs))
+  (bn_fvbn, fvbn_names, eqs)
 end
 *}
 
@@ -220,21 +220,22 @@
 *}
 
 ML {*
-fun define_raw_fv dt_info bns bmlll lthy =
+fun define_raw_fv dt_info bn_funs bclauses lthy =
 let
   val thy = ProofContext.theory_of lthy;
-  val {descr, sorts, ...} = dt_info;
-
-  val fv_names = prefix_dt_names descr sorts "fv_"
+  val {descr as dt_descr, sorts, ...} = dt_info;
 
-  val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) descr;
+  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_frees = map Free (fv_names ~~ fv_types);
-  val (bn_fvbn, (fv_bn_names, fv_bn_eqs)) = fv_bns thy dt_info fv_frees bns bmlll;
+
+  val (bn_fvbn, fv_bn_names, fv_bn_eqs) = 
+    fv_bns thy dt_info fv_frees bn_funs bclauses;
 
   val fvbns = map snd bn_fvbn;
   val fv_nums = 0 upto (length fv_frees - 1)
 
-  val fv_eqs = map2 (fv thy dt_info fv_frees bn_fvbn) bmlll (fv_frees ~~ fv_nums);
+  val fv_eqs = map2 (fv thy dt_info fv_frees bn_fvbn) bclauses (fv_frees ~~ fv_nums);
   val fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
   val fv_eqs_binds = map (fn x => (Attrib.empty_binding, x)) (flat fv_eqs @ flat fv_bn_eqs)