diff -r bc075a4ef02f -r f03bfddc5aea Nominal/Parser.thy
--- a/Nominal/Parser.thy	Fri Apr 30 10:32:34 2010 +0200
+++ b/Nominal/Parser.thy	Fri Apr 30 10:48:48 2010 +0200
@@ -389,7 +389,6 @@
   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) =
     define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3;
-  val (fv_ts_nobn, fv_ts_bn) = 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);
@@ -403,7 +402,7 @@
   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) (fv_ts_nobn @ fv_ts_bn) lthy5
+  val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) ordered_fv_ts 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
@@ -439,7 +438,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) fv_ts lthy9;
+    (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) ordered_fv_ts 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;