--- a/Nominal/NewParser.thy	Fri Apr 30 10:48:48 2010 +0200
+++ b/Nominal/NewParser.thy	Fri Apr 30 13:57:59 2010 +0200
@@ -267,6 +267,15 @@
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
   val {descr, sorts, ...} = dtinfo;
 
+  val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
+  val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames;
+  val inject = flat (map #inject dtinfos);
+  val distincts = flat (map #distinct dtinfos);
+  val rel_dtinfos = List.take (dtinfos, (length dts));
+  val rel_distinct = map #distinct rel_dtinfos;
+  val induct = #induct dtinfo;
+  val exhausts = map #exhaust dtinfos;
+
   val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1;
 
@@ -277,11 +286,13 @@
   val thy = Local_Theory.exit_global lthy2;
   val lthy3 = Theory_Target.init NONE thy;
 
-  val ((fv, fvbn), fvsimps, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
-  val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy5) =
-    define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy4;
+  val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
+  val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
+    define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a;
+  val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
+
 in
-  ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy5)
+  ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4)
 end
 *}
 
@@ -468,7 +479,7 @@
 | "bn (P2 p1 p2) = bn p1 \<union> bn p2"
 
 thm fv_lam_raw.simps fv_pt_raw.simps fv_bn_raw.simps
-thm alpha_lam_raw_alpha_pt_raw_alpha_bn_raw.intros
+thm alpha_lam_raw_alpha_pt_raw_alpha_bn_raw.intros[no_vars]
 
 nominal_datatype exp =
   EVar name

--- a/Nominal/Parser.thy	Fri Apr 30 10:48:48 2010 +0200
+++ b/Nominal/Parser.thy	Fri Apr 30 13:57:59 2010 +0200
@@ -387,8 +387,10 @@
   val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
   val raw_binds_flat = map (map flat) raw_binds;
-  val ((((fv_ts, ordered_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) =
+  val ((((_, fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) =
     define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3;
+  val (fv, fvbn) = chop (length perms) fv_ts;
+
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts
   val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct;
   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
@@ -402,14 +404,13 @@
   val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4
   val _ = tracing "Proving equivariance";
   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
-  val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) ordered_fv_ts lthy5
+  val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
     else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff) lthy6 1
   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
   val _ = tracing "Proving equivalence";
-  val (rfv_ts_nobn, rfv_ts_bn) = chop (length perms) ordered_fv_ts;
-  val fv_alpha_all = combine_fv_alpha_bns (rfv_ts_nobn, rfv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
+  val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
   val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6;
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn
@@ -430,7 +431,7 @@
   val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
   val _ = map tracing (map PolyML.makestring bns_rsp_pre')
   val (bns_rsp_pre, lthy9) = fold_map (
-    fn (bn_t, i) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
+    fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
        resolve_tac bns_rsp_pre' 1)) bns lthy8;
   val bns_rsp = flat (map snd bns_rsp_pre);
   fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
@@ -438,7 +439,7 @@
   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) ordered_fv_ts lthy9;
+    (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9;
   val fv_rsp = flat (map snd fv_rsp_pre);
   val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
@@ -452,8 +453,8 @@
       in constr_rsp_tac alpha_eq_iff (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) ordered_fv_ts
-  val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ ordered_fv_ts) lthy12;
+  val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn)
+  val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12;
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) 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;