diff -r f89773ab0685 -r a2f70c09e77d Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Mon May 17 16:29:33 2010 +0200
+++ b/Nominal/NewFv.thy	Mon May 17 16:25:45 2010 +0100
@@ -195,6 +195,7 @@
     in
       (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith)))
     end;
+
   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 bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs;
@@ -242,7 +243,7 @@
 *}
 
 ML {*
-fun define_raw_fv dt_descr sorts bn_funs bclausesss lthy =
+fun define_raw_fvs dt_descr sorts bn_funs bclausesss lthy =
 let
   val thy = ProofContext.theory_of lthy;
 
@@ -251,14 +252,15 @@
   val fv_frees = map Free (fv_names ~~ fv_types);
 
   (* free variables for the bn-functions *)
-  val (bn_fvbn, fv_bn_names, fv_bn_eqs) =
+  val (bn_fvbn_map, fv_bn_names, fv_bn_eqs) =
     fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss;
 
+  val _ = tracing ("bn_fvbn_map" ^ commas (map @{make_string} bn_fvbn_map))
   
-  val fv_bns = map snd bn_fvbn;
+  val fv_bns = map snd bn_fvbn_map;
   val fv_nums = 0 upto (length fv_frees - 1)
 
-  val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclausesss (fv_frees ~~ fv_nums);
+  val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn_map) bclausesss (fv_frees ~~ fv_nums);
 
   val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
   val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
@@ -284,7 +286,7 @@
   val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp
   val simps_exp = Morphism.fact morphism (the simps)
 in
-  ((fv_frees_exp, fv_bns_exp), simps_exp, lthy'')
+  (fv_frees_exp, fv_bns_exp, simps_exp, lthy'')
 end
 *}