--- a/Nominal/Parser.thy	Thu Mar 04 15:55:53 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 04 18:57:23 2010 +0100
@@ -240,8 +240,10 @@
   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;
+  val rel_dtinfos = List.take (dtinfos, (length dts));
   val inject = flat (map #inject dtinfos);
   val distinct = flat (map #distinct dtinfos);
+  val rel_distinct = map #distinct rel_dtinfos;
   val induct = #induct dtinfo;
   val inducts = #inducts dtinfo;
   val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
@@ -261,8 +263,9 @@
   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
   val bns = raw_bn_funs ~~ bn_nos;
   val alpha_intros = #intrs alpha;
-  val alpha_cases = #elims alpha
-  val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy4
+  val alpha_cases_loc = #elims alpha
+  val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
+  val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
 (*  val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms
@@ -272,7 +275,7 @@
   val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
   val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc
   val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
-    inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6;
+    inject alpha_inj_loc distinct 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;
@@ -318,7 +321,11 @@
   val inj_unfolded = map (LocalDefs.unfold lthy17 @{thms alpha_gen}) alpha_inj
   val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded;
   val q_inj = map (LocalDefs.fold lthy17 @{thms alpha_gen}) q_inj_pre
-  val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;*)
+  val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;
+  val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
+    (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))
+  val q_dis = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy18, th))) rel_dists;
+  val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18;*)
 in
   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
 end