--- a/Nominal/Ex/SingleLet.thy	Mon May 17 16:29:33 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Mon May 17 16:25:45 2010 +0100
@@ -30,6 +30,7 @@
 
 
 
+
 end
 
 

--- 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
 *}
 

--- a/Nominal/NewParser.thy	Mon May 17 16:29:33 2010 +0200
+++ b/Nominal/NewParser.thy	Mon May 17 16:25:45 2010 +0100
@@ -406,12 +406,11 @@
   val lthy3 = Theory_Target.init NONE thy;
   val raw_bn_funs = map (fn (f, _, _) => f) raw_bns;
 
-  val ((fv, fvbn), fv_def, lthy3a) = 
+  val (fv, fvbn, fv_def, lthy3a) = 
     if get_STEPS lthy2 > 3 
-    then define_raw_fv descr sorts raw_bns raw_bclauses lthy3
+    then define_raw_fvs descr sorts raw_bns raw_bclauses lthy3
     else raise TEST lthy3
   
-
   (* definition of raw alphas *)
   val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
     if get_STEPS lthy > 4