--- a/Nominal/Parser.thy	Thu Mar 25 15:06:58 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 25 17:30:46 2010 +0100
@@ -287,8 +287,6 @@
 *}
 
 ML {* val cheat_equivp = Unsynchronized.ref false *}
-ML {* val cheat_bn_eqvt = Unsynchronized.ref false *}
-ML {* val cheat_fv_eqvt = Unsynchronized.ref false *}
 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
 ML {* val cheat_bn_rsp = Unsynchronized.ref false *}
 ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
@@ -314,8 +312,9 @@
   val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names);
-  val descr = #descr dtinfo;
-  val sorts = #sorts dtinfo;
+  val {descr, sorts, ...} = dtinfo;
+  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+  val raw_tys = map (fn (i, _) => nth_dtyp i) descr;
   val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames;
@@ -345,39 +344,26 @@
     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
   val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4
   val _ = tracing "Proving equivariance";
-  fun build_bv_eqvt simps inducts (t, n) ctxt =
-    build_eqvts Binding.empty [t]
-      (if !cheat_bn_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
-       else build_eqvts_tac (nth inducts n) simps ctxt
-      ) ctxt
-  val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
-  val fv_eqvt_tac =
-    if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
-    else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) lthy5
-  val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_nobn fv_eqvt_tac lthy5;
-  val (fv_bn_eqvts, lthy6a) =
-    if fv_ts_bn = [] then ([], lthy6) else
-    fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) inducts)
-      (fv_ts_bn ~~ bn_nos) lthy6;
-  val raw_fv_bv_eqvt = flat (map snd bv_eqvts) @ (snd fv_eqvts) @ flat (map snd fv_bn_eqvts)
+  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
   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 @ raw_fv_bv_eqvt) lthy6a 1
-  val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a;
+    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 reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6a;
+  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 lthy6a) alpha_ts_nobn
+    if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn
     else build_equivps alpha_ts reflps alpha_induct
-      inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a;
+      inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
   val lthy7 = define_quotient_type
     (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn))
-    (ALLGOALS (resolve_tac alpha_equivp)) lthy6a;
+    (ALLGOALS (resolve_tac alpha_equivp)) lthy6;
   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
   val raw_consts =
     flat (map (fn (i, (_, _, l)) =>
@@ -455,7 +441,7 @@
   val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
   val q_dis = map (lift_thm lthy18) rel_dists;
   val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
-  val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt;
+  val q_eqvt = map (lift_thm lthy19) (bv_eqvt @ fv_eqvt);
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
   val _ = tracing "Finite Support";