--- a/Nominal/Parser.thy	Thu Mar 18 07:35:44 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 18 07:43:44 2010 +0100
@@ -329,8 +329,7 @@
   val alpha_cases_loc = #elims alpha
   val alpha_intros = ProofContext.export lthy4 lthy3 alpha_intros_loc
   val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
-  val alpha_inj_loc = build_alpha_inj alpha_intros_loc (inject @ distincts) alpha_cases_loc lthy4
-  val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
+  val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4
   val _ = tracing "Proving equivariance";
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
   val fv_eqvt_tac =
@@ -344,13 +343,13 @@
   val raw_fv_bv_eqvt = flat (map snd bv_eqvts) @ (snd fv_eqvts) @ flat (map snd fv_bn_eqvts)
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
-    else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_inj @ raw_fv_bv_eqvt) lthy6a 1
+    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;
   val _ = tracing "Proving equivalence";
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn
     else build_equivps alpha_ts induct alpha_induct
-      inject alpha_inj distincts alpha_cases alpha_eqvt lthy6a;
+      inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a;
   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
@@ -377,7 +376,7 @@
   val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
   fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy
-    else constr_rsp_tac alpha_inj (fv_rsp @ bns_rsp) alpha_equivp 1
+    else constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp) alpha_equivp 1
   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
     const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11
   val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts
@@ -403,13 +402,13 @@
   val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
   val q_bn = map (lift_thm lthy16) raw_bn_eqs;
   val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16;
-  val _ = tracing "Lifting pseudo-injectivity";
-  val inj_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_inj
-  val inj_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) inj_unfolded1
-  val q_inj_pre1 = map (lift_thm lthy17) inj_unfolded2;
-  val q_inj_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_inj_pre1
-  val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre2
-  val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;
+  val _ = tracing "Lifting eq-iff";
+  val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_eq_iff
+  val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) eq_iff_unfolded1
+  val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2;
+  val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_eq_iff_pre1
+  val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_eq_iff_pre2
+  val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_eq_iff"), []), q_eq_iff) lthy17;
   val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
     (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))
   val q_dis = map (lift_thm lthy18) rel_dists;