--- a/Nominal/Parser.thy	Mon Mar 15 17:52:31 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 15 23:42:56 2010 +0100
@@ -279,6 +279,8 @@
 ML {* val cheat_fv_rsp = ref true *}
 ML {* val cheat_const_rsp = ref true *} (* For alpha_bn 0 and alpha_bn_rsp *)
 
+ML {* val cheat_equivp = ref true *}
+
 (* Fixes for these 2 are known *)
 ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
 ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
@@ -317,8 +319,8 @@
   val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms)
   val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
   val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc;
-  val fv_ts_loc_nobn = List.take (fv_ts_loc, length perms)
-  val fv_ts_nobn = List.take (fv_ts, length perms)
+  val (fv_ts_loc_nobn, fv_ts_loc_bn) = chop (length perms) fv_ts_loc;
+  val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts;
   val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc;
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts
   val alpha_induct_loc = #induct alpha
@@ -337,18 +339,22 @@
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
     else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1
-  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc_nobn perms alpha_eqvt_tac' lthy4;
+  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy4;
   val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc;
+  val _ = map tracing (map PolyML.makestring alpha_eqvt)
   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_loc @ raw_perm_def) lthy5
-  val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5;
+  val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc_nobn fv_eqvt_tac lthy5;
+  val (fv_bn_eqvts, lthy6a) = fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts) (fv_ts_loc_bn ~~ (map snd bns)) lthy6;
+  val lthy6 = lthy6a;
   val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
   val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
-  val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc_nobn
-(*  val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
-    inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;*)
+  val alpha_equivp_loc = 
+    if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_loc_nobn
+    else build_equivps alpha_ts_loc induct alpha_induct_loc
+      inject alpha_inj_loc distincts alpha_cases_loc alpha_eqvt_loc lthy6;
   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
@@ -394,8 +400,10 @@
   val q_name = space_implode "_" qty_names;
   val q_induct = lift_thm lthy13 induct;
   val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13;
+  val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct
+  val (_, lthy14a) = Local_Theory.note ((Binding.name (q_name ^ "_inducts"), []), q_inducts) lthy14;
   val q_perm = map (lift_thm lthy14) raw_perm_def;
-  val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14;
+  val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14a;
   val q_fv = map (lift_thm lthy15) fv_def;
   val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
   val q_bn = map (lift_thm lthy16) raw_bn_eqs;