--- a/Nominal/NewParser.thy	Sun May 23 02:15:24 2010 +0100
+++ b/Nominal/NewParser.thy	Mon May 24 20:02:37 2010 +0100
@@ -343,19 +343,18 @@
   (* definition of raw fv_functions *)
   val lthy3 = Theory_Target.init NONE thy;
 
-  val (fv, fv_bn, fv_def, lthy3a) = 
+  val (raw_fvs, raw_fv_bns, raw_fv_defs, lthy3a) = 
     if get_STEPS lthy2 > 3 
     then define_raw_fvs descr sorts raw_bn_info 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 
-    then define_raw_alpha descr sorts raw_bn_info raw_bclauses fv lthy3a
+    then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs raw_fv_bns lthy3a
     else raise TEST lthy3a
   
-  val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
+  val (alpha_ts_nobn, alpha_ts_bn) = chop (length raw_fvs) alpha_ts
   
   val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr;
   val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
@@ -377,12 +376,12 @@
   (* proving equivariance lemmas *)
   val _ = warning "Proving equivariance";
   val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm ((*raw_bn_eqs @*) raw_perm_defs) (map fst bns) lthy4
-  val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fv_bn) lthy5
+  val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (raw_fv_defs @ raw_perm_defs) (raw_fvs @ raw_fv_bns) lthy5
   val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6;
 
   (* proving alpha equivalence *)
   val _ = warning "Proving equivalence";
-  val fv_alpha_all = combine_fv_alpha_bns (fv, fv_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
+  val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
   val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a;
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts
@@ -407,11 +406,11 @@
   val bns_rsp = flat (map snd bns_rsp_pre);
 
   fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
-    else fvbv_rsp_tac alpha_induct fv_def lthy8 1;
+    else fvbv_rsp_tac alpha_induct raw_fv_defs lthy8 1;
   val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
   val (fv_rsp_pre, lthy10) = fold_map
     (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
-    (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fv_bn) lthy9;
+    (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (raw_fvs @ raw_fv_bns) lthy9;
   val fv_rsp = flat (map snd fv_rsp_pre);
   val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
@@ -425,8 +424,8 @@
       in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
     const_rsp_tac) raw_consts lthy11a
-    val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fv_bn)
-  val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fv_bn)) lthy12;
+    val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns)
+  val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (raw_fvs @ raw_fv_bns)) lthy12;
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts;
   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
   val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ [] (*raw_bn_funs*)) lthy12a;
@@ -450,11 +449,11 @@
   val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",
     [Attrib.internal (K (Rule_Cases.case_names constr_names))]), 
     [Rule_Cases.name constr_names q_induct]) lthy13;
-  val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct
+  val q_inducts = Project_Rule.projects lthy13 (1 upto (length raw_fvs)) q_induct
   val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
   val q_perm = map (lift_thm qtys lthy14) raw_perm_defs;
   val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
-  val q_fv = map (lift_thm qtys lthy15) fv_def;
+  val q_fv = map (lift_thm qtys lthy15) raw_fv_defs;
   val lthy16 = note_simp_suffix "fv" q_fv lthy15;
   val q_bn = map (lift_thm qtys lthy16) [] (*raw_bn_eqs;*)
   val lthy17 = note_simp_suffix "bn" q_bn lthy16;